:: MATHMORP semantic presentation begin definition let T be non empty addMagma ; let p be Element of T; let X be Subset of T; funcX + p -> Subset of T equals :: MATHMORP:def 1 { (q + p) where q is Element of T : q in X } ; coherence { (q + p) where q is Element of T : q in X } is Subset of T proof now__::_thesis:_for_x_being_set_st_x_in__{__(q_+_p)_where_q_is_Point_of_T_:_q_in_X__}__holds_ x_in_the_carrier_of_T let x be set ; ::_thesis: ( x in { (q + p) where q is Point of T : q in X } implies x in the carrier of T ) assume x in { (q + p) where q is Point of T : q in X } ; ::_thesis: x in the carrier of T then ex q being Point of T st ( x = q + p & q in X ) ; hence x in the carrier of T ; ::_thesis: verum end; hence { (q + p) where q is Element of T : q in X } is Subset of T by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines + MATHMORP:def_1_:_ for T being non empty addMagma for p being Element of T for X being Subset of T holds X + p = { (q + p) where q is Element of T : q in X } ; definition let T be non empty addLoopStr ; let X be Subset of T; funcX ! -> Subset of T equals :: MATHMORP:def 2 { (- q) where q is Point of T : q in X } ; coherence { (- q) where q is Point of T : q in X } is Subset of T proof now__::_thesis:_for_x_being_set_st_x_in__{__(-_q)_where_q_is_Point_of_T_:_q_in_X__}__holds_ x_in_the_carrier_of_T let x be set ; ::_thesis: ( x in { (- q) where q is Point of T : q in X } implies x in the carrier of T ) assume x in { (- q) where q is Point of T : q in X } ; ::_thesis: x in the carrier of T then ex q being Point of T st ( x = - q & q in X ) ; hence x in the carrier of T ; ::_thesis: verum end; hence { (- q) where q is Point of T : q in X } is Subset of T by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines ! MATHMORP:def_2_:_ for T being non empty addLoopStr for X being Subset of T holds X ! = { (- q) where q is Point of T : q in X } ; definition let T be non empty addMagma ; let X, B be Subset of T; funcX (-) B -> Subset of T equals :: MATHMORP:def 3 { y where y is Point of T : B + y c= X } ; coherence { y where y is Point of T : B + y c= X } is Subset of T proof now__::_thesis:_for_x_being_set_st_x_in__{__y_where_y_is_Point_of_T_:_B_+_y_c=_X__}__holds_ x_in_the_carrier_of_T let x be set ; ::_thesis: ( x in { y where y is Point of T : B + y c= X } implies x in the carrier of T ) assume x in { y where y is Point of T : B + y c= X } ; ::_thesis: x in the carrier of T then ex q being Point of T st ( x = q & B + q c= X ) ; hence x in the carrier of T ; ::_thesis: verum end; hence { y where y is Point of T : B + y c= X } is Subset of T by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines (-) MATHMORP:def_3_:_ for T being non empty addMagma for X, B being Subset of T holds X (-) B = { y where y is Point of T : B + y c= X } ; notation let T be non empty addLoopStr ; let A, B be Subset of T; synonym A (+) B for A + B; end; theorem Th1: :: MATHMORP:1 for T being non empty right_complementable add-associative right_zeroed RLSStruct for B being Subset of T holds (B !) ! = B proof let T be non empty right_complementable add-associative right_zeroed RLSStruct ; ::_thesis: for B being Subset of T holds (B !) ! = B let B be Subset of T; ::_thesis: (B !) ! = B thus (B !) ! c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= (B !) ! proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B !) ! or x in B ) assume x in (B !) ! ; ::_thesis: x in B then consider q being Element of T such that A1: x = - q and A2: q in B ! ; ex q1 being Element of T st ( q = - q1 & q1 in B ) by A2; hence x in B by A1, RLVECT_1:17; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in (B !) ! ) assume A3: x in B ; ::_thesis: x in (B !) ! then reconsider xx = x as Point of T ; - xx in { (- q) where q is Point of T : q in B } by A3; then - (- xx) in { (- q) where q is Point of T : q in B ! } ; hence x in (B !) ! by RLVECT_1:17; ::_thesis: verum end; theorem Th2: :: MATHMORP:2 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for x being Point of T holds {(0. T)} + x = {x} proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x being Point of T holds {(0. T)} + x = {x} let x be Point of T; ::_thesis: {(0. T)} + x = {x} thus {(0. T)} + x c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= {(0. T)} + x proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(0. T)} + x or a in {x} ) assume a in {(0. T)} + x ; ::_thesis: a in {x} then consider q being Point of T such that A1: a = q + x and A2: q in {(0. T)} ; {q} c= {(0. T)} by A2, ZFMISC_1:31; then q = 0. T by ZFMISC_1:18; then {a} c= {x} by A1, RLVECT_1:4; hence a in {x} by ZFMISC_1:31; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in {(0. T)} + x ) assume a in {x} ; ::_thesis: a in {(0. T)} + x then {a} c= {x} by ZFMISC_1:31; then a = x by ZFMISC_1:18; then A3: a = (0. T) + x by RLVECT_1:4; 0. T in {(0. T)} by ZFMISC_1:31; hence a in {(0. T)} + x by A3; ::_thesis: verum end; theorem Th3: :: MATHMORP:3 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B1, B2 being Subset of T for p being Point of T st B1 c= B2 holds B1 + p c= B2 + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B1, B2 being Subset of T for p being Point of T st B1 c= B2 holds B1 + p c= B2 + p let B1, B2 be Subset of T; ::_thesis: for p being Point of T st B1 c= B2 holds B1 + p c= B2 + p let p be Point of T; ::_thesis: ( B1 c= B2 implies B1 + p c= B2 + p ) assume A1: B1 c= B2 ; ::_thesis: B1 + p c= B2 + p let p1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not p1 in B1 + p or p1 in B2 + p ) assume p1 in B1 + p ; ::_thesis: p1 in B2 + p then ex p2 being Point of T st ( p1 = p2 + p & p2 in B1 ) ; hence p1 in B2 + p by A1; ::_thesis: verum end; theorem Th4: :: MATHMORP:4 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for x being Point of T for X being Subset of T st X = {} holds X + x = {} proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x being Point of T for X being Subset of T st X = {} holds X + x = {} let x be Point of T; ::_thesis: for X being Subset of T st X = {} holds X + x = {} let X be Subset of T; ::_thesis: ( X = {} implies X + x = {} ) assume A1: X = {} ; ::_thesis: X + x = {} now__::_thesis:_for_y_being_set_holds_not_y_in_X_+_x given y being set such that A2: y in X + x ; ::_thesis: contradiction ex y1 being Point of T st ( y = y1 + x & y1 in X ) by A2; hence contradiction by A1; ::_thesis: verum end; hence X + x = {} by XBOOLE_0:def_1; ::_thesis: verum end; theorem :: MATHMORP:5 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T holds X (-) {(0. T)} = X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (-) {(0. T)} = X let X be Subset of T; ::_thesis: X (-) {(0. T)} = X thus X (-) {(0. T)} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (-) {(0. T)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) {(0. T)} or x in X ) assume x in X (-) {(0. T)} ; ::_thesis: x in X then ex y being Point of T st ( x = y & {(0. T)} + y c= X ) ; then {x} c= X by Th2; hence x in X by ZFMISC_1:31; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (-) {(0. T)} ) assume A1: x in X ; ::_thesis: x in X (-) {(0. T)} then reconsider xx = x as Point of T ; {x} c= X by A1, ZFMISC_1:31; then {(0. T)} + xx c= X by Th2; hence x in X (-) {(0. T)} ; ::_thesis: verum end; Lm1: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for x, y being Point of T holds {x} + y = {y} + x proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x, y being Point of T holds {x} + y = {y} + x let x, y be Point of T; ::_thesis: {x} + y = {y} + x thus {x} + y c= {y} + x :: according to XBOOLE_0:def_10 ::_thesis: {y} + x c= {x} + y proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {x} + y or x1 in {y} + x ) assume x1 in {x} + y ; ::_thesis: x1 in {y} + x then consider p1 being Point of T such that A1: x1 = p1 + y and A2: p1 in {x} ; {p1} c= {x} by A2, ZFMISC_1:31; then A3: x1 = x + y by A1, ZFMISC_1:18; y in {y} by TARSKI:def_1; hence x1 in {y} + x by A3; ::_thesis: verum end; let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {y} + x or x1 in {x} + y ) assume x1 in {y} + x ; ::_thesis: x1 in {x} + y then consider p1 being Point of T such that A4: x1 = p1 + x and A5: p1 in {y} ; {p1} c= {y} by A5, ZFMISC_1:31; then A6: x1 = x + y by A4, ZFMISC_1:18; x in {x} by TARSKI:def_1; hence x1 in {x} + y by A6; ::_thesis: verum end; theorem :: MATHMORP:6 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T holds X (+) {(0. T)} = X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (+) {(0. T)} = X let X be Subset of T; ::_thesis: X (+) {(0. T)} = X thus X (+) {(0. T)} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (+) {(0. T)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) {(0. T)} or x in X ) assume x in X (+) {(0. T)} ; ::_thesis: x in X then consider y, z being Point of T such that A1: ( x = y + z & y in X ) and A2: z in {(0. T)} ; {z} c= {(0. T)} by A2, ZFMISC_1:31; then z = 0. T by ZFMISC_1:18; hence x in X by A1, RLVECT_1:4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (+) {(0. T)} ) assume A3: x in X ; ::_thesis: x in X (+) {(0. T)} then reconsider x = x as Point of T ; 0. T in {(0. T)} by TARSKI:def_1; then x + (0. T) in { (y + z) where y, z is Point of T : ( y in X & z in {(0. T)} ) } by A3; hence x in X (+) {(0. T)} by RLVECT_1:4; ::_thesis: verum end; theorem :: MATHMORP:7 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T for x being Point of T holds X (+) {x} = X + x proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T for x being Point of T holds X (+) {x} = X + x let X be Subset of T; ::_thesis: for x being Point of T holds X (+) {x} = X + x let x be Point of T; ::_thesis: X (+) {x} = X + x thus X (+) {x} c= X + x :: according to XBOOLE_0:def_10 ::_thesis: X + x c= X (+) {x} proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) {x} or p in X + x ) assume p in X (+) {x} ; ::_thesis: p in X + x then consider y, z being Point of T such that A1: p = y + z and A2: y in X and A3: z in {x} ; {z} c= {x} by A3, ZFMISC_1:31; then p = y + x by A1, ZFMISC_1:18; hence p in X + x by A2; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X + x or p in X (+) {x} ) assume p in X + x ; ::_thesis: p in X (+) {x} then A4: ex q being Point of T st ( p = q + x & q in X ) ; x in {x} by TARSKI:def_1; hence p in X (+) {x} by A4; ::_thesis: verum end; theorem Th8: :: MATHMORP:8 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T st Y = {} holds X (-) Y = the carrier of T proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T st Y = {} holds X (-) Y = the carrier of T let X, Y be Subset of T; ::_thesis: ( Y = {} implies X (-) Y = the carrier of T ) assume A1: Y = {} ; ::_thesis: X (-) Y = the carrier of T { y where y is Point of T : Y + y c= X } = the carrier of T proof thus { y where y is Point of T : Y + y c= X } c= the carrier of T :: according to XBOOLE_0:def_10 ::_thesis: the carrier of T c= { y where y is Point of T : Y + y c= X } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of T : Y + y c= X } or x in the carrier of T ) assume x in { y where y is Point of T : Y + y c= X } ; ::_thesis: x in the carrier of T then ex y being Point of T st ( x = y & Y + y c= X ) ; hence x in the carrier of T ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of T or x in { y where y is Point of T : Y + y c= X } ) assume x in the carrier of T ; ::_thesis: x in { y where y is Point of T : Y + y c= X } then reconsider a = x as Point of T ; Y + a = {} by A1, Th4; then Y + a c= X by XBOOLE_1:2; hence x in { y where y is Point of T : Y + y c= X } ; ::_thesis: verum end; hence X (-) Y = the carrier of T ; ::_thesis: verum end; theorem Th9: :: MATHMORP:9 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, B being Subset of T st X c= Y holds ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T st X c= Y holds ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) let X, Y, B be Subset of T; ::_thesis: ( X c= Y implies ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) ) assume A1: X c= Y ; ::_thesis: ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) thus X (-) B c= Y (-) B ::_thesis: X (+) B c= Y (+) B proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B or p in Y (-) B ) assume p in X (-) B ; ::_thesis: p in Y (-) B then consider p1 being Point of T such that A2: p = p1 and A3: B + p1 c= X ; B + p1 c= Y by A1, A3, XBOOLE_1:1; hence p in Y (-) B by A2; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) B or p in Y (+) B ) assume p in X (+) B ; ::_thesis: p in Y (+) B then ex p1, p2 being Point of T st ( p = p1 + p2 & p1 in X & p2 in B ) ; hence p in Y (+) B by A1; ::_thesis: verum end; theorem Th10: :: MATHMORP:10 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B1, B2, X being Subset of T st B1 c= B2 holds ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B1, B2, X being Subset of T st B1 c= B2 holds ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 ) let B1, B2, X be Subset of T; ::_thesis: ( B1 c= B2 implies ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 ) ) assume A1: B1 c= B2 ; ::_thesis: ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 ) thus X (-) B2 c= X (-) B1 ::_thesis: X (+) B1 c= X (+) B2 proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B2 or p in X (-) B1 ) assume p in X (-) B2 ; ::_thesis: p in X (-) B1 then consider p1 being Point of T such that A2: p = p1 and A3: B2 + p1 c= X ; B1 + p1 c= B2 + p1 by A1, Th3; then B1 + p1 c= X by A3, XBOOLE_1:1; hence p in X (-) B1 by A2; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) B1 or p in X (+) B2 ) assume p in X (+) B1 ; ::_thesis: p in X (+) B2 then ex x, b being Point of T st ( p = x + b & x in X & b in B1 ) ; hence p in X (+) B2 by A1; ::_thesis: verum end; theorem :: MATHMORP:11 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, X being Subset of T st 0. T in B holds ( X (-) B c= X & X c= X (+) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X being Subset of T st 0. T in B holds ( X (-) B c= X & X c= X (+) B ) let B, X be Subset of T; ::_thesis: ( 0. T in B implies ( X (-) B c= X & X c= X (+) B ) ) assume A1: 0. T in B ; ::_thesis: ( X (-) B c= X & X c= X (+) B ) thus X (-) B c= X ::_thesis: X c= X (+) B proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B or p in X ) assume p in X (-) B ; ::_thesis: p in X then consider p1 being Point of T such that A2: p = p1 and A3: B + p1 c= X ; (0. T) + p1 in { (q + p1) where q is Point of T : q in B } by A1; then (0. T) + p1 in X by A3; hence p in X by A2, RLVECT_1:4; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X or p in X (+) B ) assume A4: p in X ; ::_thesis: p in X (+) B then reconsider p = p as Point of T ; p + (0. T) in { (x + b) where x, b is Point of T : ( x in X & b in B ) } by A1, A4; hence p in X (+) B by RLVECT_1:4; ::_thesis: verum end; theorem Th12: :: MATHMORP:12 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T holds X (+) Y = Y (+) X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds X (+) Y = Y (+) X let X, Y be Subset of T; ::_thesis: X (+) Y = Y (+) X thus X (+) Y c= Y (+) X :: according to XBOOLE_0:def_10 ::_thesis: Y (+) X c= X (+) Y proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) Y or p in Y (+) X ) assume p in X (+) Y ; ::_thesis: p in Y (+) X then ex p1, p2 being Point of T st ( p = p1 + p2 & p1 in X & p2 in Y ) ; hence p in Y (+) X ; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y (+) X or p in X (+) Y ) assume p in Y (+) X ; ::_thesis: p in X (+) Y then ex p1, p2 being Point of T st ( p = p1 + p2 & p1 in Y & p2 in X ) ; hence p in X (+) Y ; ::_thesis: verum end; Lm2: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for p, x being Point of T holds ( (p - x) + x = p & (p + x) - x = p ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for p, x being Point of T holds ( (p - x) + x = p & (p + x) - x = p ) let p, x be Point of T; ::_thesis: ( (p - x) + x = p & (p + x) - x = p ) (p + x) - x = p + (x - x) by RLVECT_1:def_3 .= p + (0. T) by RLVECT_1:15 .= p by RLVECT_1:4 ; hence ( (p - x) + x = p & (p + x) - x = p ) by RLVECT_1:28; ::_thesis: verum end; theorem Th13: :: MATHMORP:13 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for Y, X being Subset of T for y, x being Point of T holds ( Y + y c= X + x iff Y + (y - x) c= X ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for Y, X being Subset of T for y, x being Point of T holds ( Y + y c= X + x iff Y + (y - x) c= X ) let Y, X be Subset of T; ::_thesis: for y, x being Point of T holds ( Y + y c= X + x iff Y + (y - x) c= X ) let y, x be Point of T; ::_thesis: ( Y + y c= X + x iff Y + (y - x) c= X ) thus ( Y + y c= X + x implies Y + (y - x) c= X ) ::_thesis: ( Y + (y - x) c= X implies Y + y c= X + x ) proof assume A1: Y + y c= X + x ; ::_thesis: Y + (y - x) c= X let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y + (y - x) or p in X ) assume p in Y + (y - x) ; ::_thesis: p in X then consider q1 being Point of T such that A2: p = q1 + (y - x) and A3: q1 in Y ; reconsider p = p as Point of T by A2; p = (q1 + y) - x by A2, RLVECT_1:28; then A4: p + x = q1 + y by Lm2; q1 + y in { (q + y) where q is Point of T : q in Y } by A3; then p + x in X + x by A1, A4; then consider p1 being Point of T such that A5: p + x = p1 + x and A6: p1 in X ; (p + x) - x = p1 by A5, Lm2; hence p in X by A6, Lm2; ::_thesis: verum end; assume A7: Y + (y - x) c= X ; ::_thesis: Y + y c= X + x let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y + y or p in X + x ) assume p in Y + y ; ::_thesis: p in X + x then consider q1 being Point of T such that A8: p = q1 + y and A9: q1 in Y ; reconsider p = p as Point of T by A8; ( p - x = q1 + (y - x) & q1 + (y - x) in { (q + (y - x)) where q is Point of T : q in Y } ) by A8, A9, RLVECT_1:28; then (p - x) + x in { (q + x) where q is Point of T : q in X } by A7; hence p in X + x by Lm2; ::_thesis: verum end; theorem Th14: :: MATHMORP:14 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p let p be Point of T; ::_thesis: (X + p) (-) Y = (X (-) Y) + p thus (X + p) (-) Y c= (X (-) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) + p c= (X + p) (-) Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X + p) (-) Y or x in (X (-) Y) + p ) assume x in (X + p) (-) Y ; ::_thesis: x in (X (-) Y) + p then consider y being Point of T such that A1: x = y and A2: Y + y c= X + p ; Y + (y - p) c= X by A2, Th13; then y - p in { y1 where y1 is Point of T : Y + y1 c= X } ; then (y - p) + p in { (q + p) where q is Point of T : q in X (-) Y } ; hence x in (X (-) Y) + p by A1, Lm2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) Y) + p or x in (X + p) (-) Y ) assume x in (X (-) Y) + p ; ::_thesis: x in (X + p) (-) Y then consider y being Point of T such that A3: x = y + p and A4: y in X (-) Y ; reconsider x = x as Point of T by A3; ( x - p = y & ex y2 being Point of T st ( y = y2 & Y + y2 c= X ) ) by A3, A4, Lm2; then Y + x c= X + p by Th13; hence x in (X + p) (-) Y ; ::_thesis: verum end; theorem Th15: :: MATHMORP:15 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p let p be Point of T; ::_thesis: (X + p) (+) Y = (X (+) Y) + p thus (X + p) (+) Y c= (X (+) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) + p c= (X + p) (+) Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X + p) (+) Y or x in (X (+) Y) + p ) assume x in (X + p) (+) Y ; ::_thesis: x in (X (+) Y) + p then consider x2, y2 being Point of T such that A1: x = x2 + y2 and A2: x2 in X + p and A3: y2 in Y ; consider x3 being Point of T such that A4: ( x2 = x3 + p & x3 in X ) by A2; ( x = (x3 + y2) + p & x3 + y2 in X (+) Y ) by A1, A3, A4, RLVECT_1:def_3; hence x in (X (+) Y) + p ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) Y) + p or x in (X + p) (+) Y ) assume x in (X (+) Y) + p ; ::_thesis: x in (X + p) (+) Y then consider x2 being Point of T such that A5: x = x2 + p and A6: x2 in X (+) Y ; consider x3, y3 being Point of T such that A7: x2 = x3 + y3 and A8: x3 in X and A9: y3 in Y by A6; A10: x3 + p in X + p by A8; x = (x3 + p) + y3 by A5, A7, RLVECT_1:def_3; hence x in (X + p) (+) Y by A9, A10; ::_thesis: verum end; theorem Th16: :: MATHMORP:16 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T for x, y being Point of T holds (X + x) + y = X + (x + y) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T for x, y being Point of T holds (X + x) + y = X + (x + y) let X be Subset of T; ::_thesis: for x, y being Point of T holds (X + x) + y = X + (x + y) let x, y be Point of T; ::_thesis: (X + x) + y = X + (x + y) thus (X + x) + y c= X + (x + y) :: according to XBOOLE_0:def_10 ::_thesis: X + (x + y) c= (X + x) + y proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X + x) + y or p in X + (x + y) ) assume p in (X + x) + y ; ::_thesis: p in X + (x + y) then consider x2 being Point of T such that A1: p = x2 + y and A2: x2 in X + x ; consider x3 being Point of T such that A3: x2 = x3 + x and A4: x3 in X by A2; p = x3 + (x + y) by A1, A3, RLVECT_1:def_3; hence p in X + (x + y) by A4; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X + (x + y) or p in (X + x) + y ) assume p in X + (x + y) ; ::_thesis: p in (X + x) + y then consider x2 being Point of T such that A5: ( p = x2 + (x + y) & x2 in X ) ; ( p = (x2 + x) + y & x2 + x in X + x ) by A5, RLVECT_1:def_3; hence p in (X + x) + y ; ::_thesis: verum end; theorem Th17: :: MATHMORP:17 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p) let X, Y be Subset of T; ::_thesis: for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p) let p be Point of T; ::_thesis: X (-) (Y + p) = (X (-) Y) + (- p) thus X (-) (Y + p) c= (X (-) Y) + (- p) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) + (- p) c= X (-) (Y + p) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) (Y + p) or x in (X (-) Y) + (- p) ) assume x in X (-) (Y + p) ; ::_thesis: x in (X (-) Y) + (- p) then consider y being Point of T such that A1: x = y and A2: (Y + p) + y c= X ; Y + (y + p) c= X by A2, Th16; then y + p in { y1 where y1 is Point of T : Y + y1 c= X } ; then (y + p) - p in (X (-) Y) + (- p) ; hence x in (X (-) Y) + (- p) by A1, Lm2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) Y) + (- p) or x in X (-) (Y + p) ) assume x in (X (-) Y) + (- p) ; ::_thesis: x in X (-) (Y + p) then consider y being Point of T such that A3: x = y + (- p) and A4: y in X (-) Y ; reconsider x = x as Point of T by A3; x + p = (y - p) + p by A3; then A5: x + p = y by Lm2; ex y2 being Point of T st ( y = y2 & Y + y2 c= X ) by A4; then (Y + p) + x c= X by A5, Th16; hence x in X (-) (Y + p) ; ::_thesis: verum end; theorem :: MATHMORP:18 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p let X, Y be Subset of T; ::_thesis: for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p let p be Point of T; ::_thesis: X (+) (Y + p) = (X (+) Y) + p thus X (+) (Y + p) c= (X (+) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) + p c= X (+) (Y + p) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (Y + p) or x in (X (+) Y) + p ) assume x in X (+) (Y + p) ; ::_thesis: x in (X (+) Y) + p then consider x2, y2 being Point of T such that A1: ( x = x2 + y2 & x2 in X ) and A2: y2 in Y + p ; consider y3 being Point of T such that A3: ( y2 = y3 + p & y3 in Y ) by A2; ( x = (x2 + y3) + p & x2 + y3 in X (+) Y ) by A1, A3, RLVECT_1:def_3; hence x in (X (+) Y) + p ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) Y) + p or x in X (+) (Y + p) ) assume x in (X (+) Y) + p ; ::_thesis: x in X (+) (Y + p) then consider x2 being Point of T such that A4: x = x2 + p and A5: x2 in X (+) Y ; consider x3, y3 being Point of T such that A6: x2 = x3 + y3 and A7: x3 in X and A8: y3 in Y by A5; A9: y3 + p in Y + p by A8; x = x3 + (y3 + p) by A4, A6, RLVECT_1:def_3; hence x in X (+) (Y + p) by A7, A9; ::_thesis: verum end; theorem Th19: :: MATHMORP:19 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T for x being Point of T st x in X holds B + x c= B (+) X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T for x being Point of T st x in X holds B + x c= B (+) X let X, B be Subset of T; ::_thesis: for x being Point of T st x in X holds B + x c= B (+) X let x be Point of T; ::_thesis: ( x in X implies B + x c= B (+) X ) assume A1: x in X ; ::_thesis: B + x c= B (+) X let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B + x or y in B (+) X ) assume y in B + x ; ::_thesis: y in B (+) X then ex y1 being Point of T st ( y = y1 + x & y1 in B ) ; hence y in B (+) X by A1; ::_thesis: verum end; theorem Th20: :: MATHMORP:20 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds X c= (X (+) B) (-) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds X c= (X (+) B) (-) B let X, B be Subset of T; ::_thesis: X c= (X (+) B) (-) B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (X (+) B) (-) B ) assume A1: x in X ; ::_thesis: x in (X (+) B) (-) B then consider x1 being Point of T such that A2: x1 = x ; B + x1 c= B (+) X by A1, A2, Th19; then x in (B (+) X) (-) B by A2; hence x in (X (+) B) (-) B by Th12; ::_thesis: verum end; theorem Th21: :: MATHMORP:21 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T holds X + (0. T) = X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X + (0. T) = X let X be Subset of T; ::_thesis: X + (0. T) = X thus X + (0. T) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X + (0. T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X + (0. T) or x in X ) assume x in X + (0. T) ; ::_thesis: x in X then ex q being Point of T st ( x = q + (0. T) & q in X ) ; hence x in X by RLVECT_1:4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X + (0. T) ) assume A1: x in X ; ::_thesis: x in X + (0. T) then reconsider x1 = x as Point of T ; x1 = x1 + (0. T) by RLVECT_1:4; hence x in X + (0. T) by A1; ::_thesis: verum end; theorem :: MATHMORP:22 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T for x being Point of T holds X (-) {x} = X + (- x) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T for x being Point of T holds X (-) {x} = X + (- x) let X be Subset of T; ::_thesis: for x being Point of T holds X (-) {x} = X + (- x) let x be Point of T; ::_thesis: X (-) {x} = X + (- x) thus X (-) {x} c= X + (- x) :: according to XBOOLE_0:def_10 ::_thesis: X + (- x) c= X (-) {x} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X (-) {x} or y in X + (- x) ) assume y in X (-) {x} ; ::_thesis: y in X + (- x) then consider p being Point of T such that A1: p = y and A2: {x} + p c= X ; {p} + x c= X by A2, Lm1; then ({p} + x) + (- x) c= X + (- x) by Th3; then {p} + (x + (- x)) c= X + (- x) by Th16; then {p} + (0. T) c= X + (- x) by RLVECT_1:5; then {p} c= X + (- x) by Th21; hence y in X + (- x) by A1, ZFMISC_1:31; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X + (- x) or y in X (-) {x} ) assume y in X + (- x) ; ::_thesis: y in X (-) {x} then consider p being Point of T such that A3: y = p + (- x) and A4: p in X ; reconsider y = y as Point of T by A3; y = p - x by A3; then A5: y + x = p by Lm2; {x} + y c= X proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} + y or q in X ) assume q in {x} + y ; ::_thesis: q in X then consider qq being Point of T such that A6: q = qq + y and A7: qq in {x} ; {qq} c= {x} by A7, ZFMISC_1:31; hence q in X by A4, A5, A6, ZFMISC_1:18; ::_thesis: verum end; hence y in X (-) {x} ; ::_thesis: verum end; Lm3: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds (X (-) B) (+) B c= X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (-) B) (+) B c= X let X, B be Subset of T; ::_thesis: (X (-) B) (+) B c= X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) (+) B or x in X ) assume x in (X (-) B) (+) B ; ::_thesis: x in X then consider y1, y2 being Point of T such that A1: x = y1 + y2 and A2: y1 in X (-) B and A3: y2 in B ; consider y being Point of T such that A4: y1 = y and A5: B + y c= X by A2; x in B + y by A1, A3, A4; hence x in X by A5; ::_thesis: verum end; theorem Th23: :: MATHMORP:23 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z let X, Y, Z be Subset of T; ::_thesis: X (-) (Y (+) Z) = (X (-) Y) (-) Z A1: (X (-) Y) (+) Y c= X by Lm3; thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) (-) Z c= X (-) (Y (+) Z) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) (Y (+) Z) or p in (X (-) Y) (-) Z ) assume p in X (-) (Y (+) Z) ; ::_thesis: p in (X (-) Y) (-) Z then consider x being Point of T such that A2: p = x and A3: (Y (+) Z) + x c= X ; (Y + x) (+) Z c= X by A3, Th15; then Z (+) (Y + x) c= X by Th12; then A4: (Z (+) (Y + x)) (-) (Y + x) c= X (-) (Y + x) by Th9; Z c= (Z (+) (Y + x)) (-) (Y + x) by Th20; then Z c= X (-) (Y + x) by A4, XBOOLE_1:1; then Z c= (X (-) Y) + (- x) by Th17; then Z + x c= ((X (-) Y) + (- x)) + x by Th3; then Z + x c= (X (-) Y) + ((- x) + x) by Th16; then Z + x c= (X (-) Y) + (x - x) ; then Z + x c= (X (-) Y) + (0. T) by RLVECT_1:15; then Z + x c= X (-) Y by Th21; hence p in (X (-) Y) (-) Z by A2; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X (-) Y) (-) Z or p in X (-) (Y (+) Z) ) assume p in (X (-) Y) (-) Z ; ::_thesis: p in X (-) (Y (+) Z) then consider y being Point of T such that A5: p = y and A6: Z + y c= X (-) Y ; (Z + y) (+) Y c= (X (-) Y) (+) Y by A6, Th9; then (Z + y) (+) Y c= X by A1, XBOOLE_1:1; then (Z (+) Y) + y c= X by Th15; then p in X (-) (Z (+) Y) by A5; hence p in X (-) (Y (+) Z) by Th12; ::_thesis: verum end; theorem :: MATHMORP:24 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y let X, Y, Z be Subset of T; ::_thesis: X (-) (Y (+) Z) = (X (-) Z) (-) Y X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12 .= (X (-) Z) (-) Y by Th23 ; hence X (-) (Y (+) Z) = (X (-) Z) (-) Y ; ::_thesis: verum end; theorem :: MATHMORP:25 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z let X, Y, Z be Subset of T; ::_thesis: X (+) (Y (-) Z) c= (X (+) Y) (-) Z let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (Y (-) Z) or x in (X (+) Y) (-) Z ) assume x in X (+) (Y (-) Z) ; ::_thesis: x in (X (+) Y) (-) Z then consider a, b being Point of T such that A1: x = a + b and A2: a in X and A3: b in Y (-) Z ; ex c being Point of T st ( b = c & Z + c c= Y ) by A3; then (Z + b) + a c= Y + a by Th3; then A4: Z + (b + a) c= Y + a by Th16; Y + a c= Y (+) X by A2, Th19; then Z + (b + a) c= Y (+) X by A4, XBOOLE_1:1; then x in (Y (+) X) (-) Z by A1; hence x in (X (+) Y) (-) Z by Th12; ::_thesis: verum end; theorem :: MATHMORP:26 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z let X, Y, Z be Subset of T; ::_thesis: X (+) (Y (+) Z) = (X (+) Y) (+) Z thus X (+) (Y (+) Z) c= (X (+) Y) (+) Z :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) (+) Z c= X (+) (Y (+) Z) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) (Y (+) Z) or p in (X (+) Y) (+) Z ) assume p in X (+) (Y (+) Z) ; ::_thesis: p in (X (+) Y) (+) Z then consider x1, p2 being Point of T such that A1: ( p = x1 + p2 & x1 in X ) and A2: p2 in Y (+) Z ; consider y, z being Point of T such that A3: ( p2 = y + z & y in Y ) and A4: z in Z by A2; set p3 = x1 + y; ( p = (x1 + y) + z & x1 + y in X (+) Y ) by A1, A3, RLVECT_1:def_3; hence p in (X (+) Y) (+) Z by A4; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X (+) Y) (+) Z or p in X (+) (Y (+) Z) ) assume p in (X (+) Y) (+) Z ; ::_thesis: p in X (+) (Y (+) Z) then consider x1, p2 being Point of T such that A5: p = x1 + p2 and A6: x1 in X (+) Y and A7: p2 in Z ; consider y, z being Point of T such that A8: x1 = y + z and A9: y in X and A10: z in Y by A6; set p3 = z + p2; ( p = y + (z + p2) & z + p2 in Y (+) Z ) by A5, A7, A8, A10, RLVECT_1:def_3; hence p in X (+) (Y (+) Z) by A9; ::_thesis: verum end; theorem Th27: :: MATHMORP:27 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, C being Subset of T for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C being Subset of T for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y) let B, C be Subset of T; ::_thesis: for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y) let y be Point of T; ::_thesis: (B \/ C) + y = (B + y) \/ (C + y) thus (B \/ C) + y c= (B + y) \/ (C + y) :: according to XBOOLE_0:def_10 ::_thesis: (B + y) \/ (C + y) c= (B \/ C) + y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ C) + y or x in (B + y) \/ (C + y) ) assume x in (B \/ C) + y ; ::_thesis: x in (B + y) \/ (C + y) then consider y2 being Point of T such that A1: x = y2 + y and A2: y2 in B \/ C ; ( y2 in B or y2 in C ) by A2, XBOOLE_0:def_3; then ( x in { (y1 + y) where y1 is Point of T : y1 in B } or x in { (y1 + y) where y1 is Point of T : y1 in C } ) by A1; hence x in (B + y) \/ (C + y) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B + y) \/ (C + y) or x in (B \/ C) + y ) assume x in (B + y) \/ (C + y) ; ::_thesis: x in (B \/ C) + y then ( x in B + y or x in C + y ) by XBOOLE_0:def_3; then consider y2 being Point of T such that A3: ( ( x = y2 + y & y2 in B ) or ( x = y2 + y & y2 in C ) ) ; y2 in B \/ C by A3, XBOOLE_0:def_3; hence x in (B \/ C) + y by A3; ::_thesis: verum end; theorem Th28: :: MATHMORP:28 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, C being Subset of T for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C being Subset of T for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y) let B, C be Subset of T; ::_thesis: for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y) let y be Point of T; ::_thesis: (B /\ C) + y = (B + y) /\ (C + y) thus (B /\ C) + y c= (B + y) /\ (C + y) :: according to XBOOLE_0:def_10 ::_thesis: (B + y) /\ (C + y) c= (B /\ C) + y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B /\ C) + y or x in (B + y) /\ (C + y) ) assume x in (B /\ C) + y ; ::_thesis: x in (B + y) /\ (C + y) then consider y2 being Point of T such that A1: x = y2 + y and A2: y2 in B /\ C ; y2 in C by A2, XBOOLE_0:def_4; then A3: x in { (y1 + y) where y1 is Point of T : y1 in C } by A1; y2 in B by A2, XBOOLE_0:def_4; then x in { (y1 + y) where y1 is Point of T : y1 in B } by A1; hence x in (B + y) /\ (C + y) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B + y) /\ (C + y) or x in (B /\ C) + y ) assume A4: x in (B + y) /\ (C + y) ; ::_thesis: x in (B /\ C) + y then x in B + y by XBOOLE_0:def_4; then consider y3 being Point of T such that A5: x = y3 + y and A6: y3 in B ; x in C + y by A4, XBOOLE_0:def_4; then consider y2 being Point of T such that A7: x = y2 + y and A8: y2 in C ; (y2 + y) - y = y3 by A5, A7, Lm2; then A9: y2 = y3 by Lm2; then y2 in B /\ C by A6, A8, XBOOLE_0:def_4; hence x in (B /\ C) + y by A5, A9; ::_thesis: verum end; theorem :: MATHMORP:29 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C) let X, B, C be Subset of T; ::_thesis: X (-) (B \/ C) = (X (-) B) /\ (X (-) C) thus X (-) (B \/ C) c= (X (-) B) /\ (X (-) C) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) B) /\ (X (-) C) c= X (-) (B \/ C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) (B \/ C) or x in (X (-) B) /\ (X (-) C) ) assume x in X (-) (B \/ C) ; ::_thesis: x in (X (-) B) /\ (X (-) C) then consider y being Point of T such that A1: x = y and A2: (B \/ C) + y c= X ; A3: (B + y) \/ (C + y) c= X by A2, Th27; then C + y c= X by XBOOLE_1:11; then A4: x in { y1 where y1 is Point of T : C + y1 c= X } by A1; B + y c= X by A3, XBOOLE_1:11; then x in { y1 where y1 is Point of T : B + y1 c= X } by A1; hence x in (X (-) B) /\ (X (-) C) by A4, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) /\ (X (-) C) or x in X (-) (B \/ C) ) assume A5: x in (X (-) B) /\ (X (-) C) ; ::_thesis: x in X (-) (B \/ C) then x in X (-) B by XBOOLE_0:def_4; then consider y being Point of T such that A6: x = y and A7: B + y c= X ; x in X (-) C by A5, XBOOLE_0:def_4; then ex y2 being Point of T st ( x = y2 & C + y2 c= X ) ; then (B + y) \/ (C + y) c= X by A6, A7, XBOOLE_1:8; then (B \/ C) + y c= X by Th27; hence x in X (-) (B \/ C) by A6; ::_thesis: verum end; theorem :: MATHMORP:30 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C) let X, B, C be Subset of T; ::_thesis: X (+) (B \/ C) = (X (+) B) \/ (X (+) C) thus X (+) (B \/ C) c= (X (+) B) \/ (X (+) C) :: according to XBOOLE_0:def_10 ::_thesis: (X (+) B) \/ (X (+) C) c= X (+) (B \/ C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (B \/ C) or x in (X (+) B) \/ (X (+) C) ) assume x in X (+) (B \/ C) ; ::_thesis: x in (X (+) B) \/ (X (+) C) then consider y3, y4 being Point of T such that A1: ( x = y3 + y4 & y3 in X ) and A2: y4 in B \/ C ; ( y4 in B or y4 in C ) by A2, XBOOLE_0:def_3; then ( x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in B ) } or x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in C ) } ) by A1; hence x in (X (+) B) \/ (X (+) C) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) B) \/ (X (+) C) or x in X (+) (B \/ C) ) assume x in (X (+) B) \/ (X (+) C) ; ::_thesis: x in X (+) (B \/ C) then ( x in X (+) B or x in X (+) C ) by XBOOLE_0:def_3; then consider y3, y4 being Point of T such that A3: ( ( x = y3 + y4 & y3 in X & y4 in B ) or ( x = y3 + y4 & y3 in X & y4 in C ) ) ; y4 in B \/ C by A3, XBOOLE_0:def_3; hence x in X (+) (B \/ C) by A3; ::_thesis: verum end; theorem :: MATHMORP:31 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B let X, B, Y be Subset of T; ::_thesis: (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) \/ (Y (-) B) or x in (X \/ Y) (-) B ) assume x in (X (-) B) \/ (Y (-) B) ; ::_thesis: x in (X \/ Y) (-) B then ( x in X (-) B or x in Y (-) B ) by XBOOLE_0:def_3; then consider y being Point of T such that A1: ( ( x = y & B + y c= X ) or ( x = y & B + y c= Y ) ) ; B + y c= X \/ Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B + y or z in X \/ Y ) assume z in B + y ; ::_thesis: z in X \/ Y hence z in X \/ Y by A1, XBOOLE_0:def_3; ::_thesis: verum end; hence x in (X \/ Y) (-) B by A1; ::_thesis: verum end; theorem :: MATHMORP:32 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B) let X, Y, B be Subset of T; ::_thesis: (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B) thus (X \/ Y) (+) B c= (X (+) B) \/ (Y (+) B) :: according to XBOOLE_0:def_10 ::_thesis: (X (+) B) \/ (Y (+) B) c= (X \/ Y) (+) B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) (+) B or x in (X (+) B) \/ (Y (+) B) ) assume x in (X \/ Y) (+) B ; ::_thesis: x in (X (+) B) \/ (Y (+) B) then consider y1, y2 being Point of T such that A1: x = y1 + y2 and A2: y1 in X \/ Y and A3: y2 in B ; ( y1 in X or y1 in Y ) by A2, XBOOLE_0:def_3; then ( x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in X & y4 in B ) } or x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in Y & y4 in B ) } ) by A1, A3; hence x in (X (+) B) \/ (Y (+) B) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) B) \/ (Y (+) B) or x in (X \/ Y) (+) B ) assume x in (X (+) B) \/ (Y (+) B) ; ::_thesis: x in (X \/ Y) (+) B then ( x in X (+) B or x in Y (+) B ) by XBOOLE_0:def_3; then consider y1, y2 being Point of T such that A4: ( ( x = y1 + y2 & y1 in X & y2 in B ) or ( x = y1 + y2 & y1 in Y & y2 in B ) ) ; y1 in X \/ Y by A4, XBOOLE_0:def_3; hence x in (X \/ Y) (+) B by A4; ::_thesis: verum end; theorem :: MATHMORP:33 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B) let X, Y, B be Subset of T; ::_thesis: (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B) thus (X /\ Y) (-) B c= (X (-) B) /\ (Y (-) B) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) B) /\ (Y (-) B) c= (X /\ Y) (-) B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) (-) B or x in (X (-) B) /\ (Y (-) B) ) assume x in (X /\ Y) (-) B ; ::_thesis: x in (X (-) B) /\ (Y (-) B) then consider y being Point of T such that A1: x = y and A2: B + y c= X /\ Y ; B + y c= Y by A2, XBOOLE_1:18; then A3: x in { y1 where y1 is Point of T : B + y1 c= Y } by A1; B + y c= X by A2, XBOOLE_1:18; then x in { y1 where y1 is Point of T : B + y1 c= X } by A1; hence x in (X (-) B) /\ (Y (-) B) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) /\ (Y (-) B) or x in (X /\ Y) (-) B ) assume A4: x in (X (-) B) /\ (Y (-) B) ; ::_thesis: x in (X /\ Y) (-) B then x in X (-) B by XBOOLE_0:def_4; then consider y being Point of T such that A5: x = y and A6: B + y c= X ; x in Y (-) B by A4, XBOOLE_0:def_4; then A7: ex y2 being Point of T st ( x = y2 & B + y2 c= Y ) ; B + y c= X /\ Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B + y or z in X /\ Y ) assume z in B + y ; ::_thesis: z in X /\ Y hence z in X /\ Y by A5, A6, A7, XBOOLE_0:def_4; ::_thesis: verum end; hence x in (X /\ Y) (-) B by A5; ::_thesis: verum end; theorem Th34: :: MATHMORP:34 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B) let X, Y, B be Subset of T; ::_thesis: (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) (+) B or x in (X (+) B) /\ (Y (+) B) ) assume x in (X /\ Y) (+) B ; ::_thesis: x in (X (+) B) /\ (Y (+) B) then consider y1, y2 being Point of T such that A1: x = y1 + y2 and A2: y1 in X /\ Y and A3: y2 in B ; y1 in Y by A2, XBOOLE_0:def_4; then A4: x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in Y & y4 in B ) } by A1, A3; y1 in X by A2, XBOOLE_0:def_4; then x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in X & y4 in B ) } by A1, A3; hence x in (X (+) B) /\ (Y (+) B) by A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: MATHMORP:35 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) let B, X, Y be Subset of T; ::_thesis: B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) B (+) (X /\ Y) = (X /\ Y) (+) B by Th12; then B (+) (X /\ Y) c= (X (+) B) /\ (Y (+) B) by Th34; then B (+) (X /\ Y) c= (B (+) X) /\ (Y (+) B) by Th12; hence B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) by Th12; ::_thesis: verum end; theorem :: MATHMORP:36 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y) let B, X, Y be Subset of T; ::_thesis: (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B (-) X) \/ (B (-) Y) or x in B (-) (X /\ Y) ) assume x in (B (-) X) \/ (B (-) Y) ; ::_thesis: x in B (-) (X /\ Y) then ( x in B (-) X or x in B (-) Y ) by XBOOLE_0:def_3; then consider y being Point of T such that A1: ( ( x = y & X + y c= B ) or ( x = y & Y + y c= B ) ) ; (X + y) /\ (Y + y) c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (X + y) /\ (Y + y) or a in B ) assume A2: a in (X + y) /\ (Y + y) ; ::_thesis: a in B then A3: a in X + y by XBOOLE_0:def_4; A4: a in Y + y by A2, XBOOLE_0:def_4; percases ( X + y c= B or Y + y c= B ) by A1; suppose X + y c= B ; ::_thesis: a in B hence a in B by A3; ::_thesis: verum end; suppose Y + y c= B ; ::_thesis: a in B hence a in B by A4; ::_thesis: verum end; end; end; then (X /\ Y) + y c= B by Th28; hence x in B (-) (X /\ Y) by A1; ::_thesis: verum end; theorem Th37: :: MATHMORP:37 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !) let X, B be Subset of T; ::_thesis: ((X `) (-) B) ` = X (+) (B !) thus ((X `) (-) B) ` c= X (+) (B !) :: according to XBOOLE_0:def_10 ::_thesis: X (+) (B !) c= ((X `) (-) B) ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((X `) (-) B) ` or x in X (+) (B !) ) assume A1: x in ((X `) (-) B) ` ; ::_thesis: x in X (+) (B !) then reconsider x1 = x as Point of T ; not x in (X `) (-) B by A1, XBOOLE_0:def_5; then not B + x1 c= X ` ; then B + x1 meets X by SUBSET_1:23; then consider y being set such that A2: y in B + x1 and A3: y in X by XBOOLE_0:3; reconsider y1 = y as Point of T by A2; consider b1 being Point of T such that A4: ( y = b1 + x1 & b1 in B ) by A2; ( x1 = y1 - b1 & - b1 in B ! ) by A4, Lm2; hence x in X (+) (B !) by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (B !) or x in ((X `) (-) B) ` ) assume x in X (+) (B !) ; ::_thesis: x in ((X `) (-) B) ` then consider x1, b1 being Point of T such that A5: x = x1 + b1 and A6: x1 in X and A7: b1 in B ! ; reconsider xx = x as Point of T by A5; consider b2 being Point of T such that A8: b1 = - b2 and A9: b2 in B by A7; x = x1 - b2 by A5, A8; then A10: xx + b2 = x1 by Lm2; b2 + xx in { (pb + xx) where pb is Point of T : pb in B } by A9; then A11: B + xx meets X by A6, A10, XBOOLE_0:3; not xx in (X `) (-) B proof assume xx in (X `) (-) B ; ::_thesis: contradiction then ex yy being Point of T st ( xx = yy & B + yy c= X ` ) ; hence contradiction by A11, SUBSET_1:23; ::_thesis: verum end; hence x in ((X `) (-) B) ` by XBOOLE_0:def_5; ::_thesis: verum end; theorem Th38: :: MATHMORP:38 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !) let X, B be Subset of T; ::_thesis: (X (-) B) ` = (X `) (+) (B !) thus (X (-) B) ` c= (X `) (+) (B !) :: according to XBOOLE_0:def_10 ::_thesis: (X `) (+) (B !) c= (X (-) B) ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) ` or x in (X `) (+) (B !) ) assume A1: x in (X (-) B) ` ; ::_thesis: x in (X `) (+) (B !) then reconsider x1 = x as Point of T ; not x in X (-) B by A1, XBOOLE_0:def_5; then not B + x1 c= X ; then B + x1 meets X ` by SUBSET_1:24; then consider y being set such that A2: y in B + x1 and A3: y in X ` by XBOOLE_0:3; reconsider y1 = y as Point of T by A2; consider b1 being Point of T such that A4: ( y = b1 + x1 & b1 in B ) by A2; ( x1 = y1 - b1 & - b1 in B ! ) by A4, Lm2; hence x in (X `) (+) (B !) by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X `) (+) (B !) or x in (X (-) B) ` ) assume x in (X `) (+) (B !) ; ::_thesis: x in (X (-) B) ` then consider x1, b1 being Point of T such that A5: x = x1 + b1 and A6: x1 in X ` and A7: b1 in B ! ; reconsider xx = x as Point of T by A5; consider q being Point of T such that A8: b1 = - q and A9: q in B by A7; xx = x1 - q by A5, A8; then A10: xx + q = x1 by Lm2; q + xx in { (q1 + xx) where q1 is Point of T : q1 in B } by A9; then A11: B + xx meets X ` by A6, A10, XBOOLE_0:3; not xx in X (-) B proof assume xx in X (-) B ; ::_thesis: contradiction then ex yy being Point of T st ( xx = yy & B + yy c= X ) ; hence contradiction by A11, SUBSET_1:24; ::_thesis: verum end; hence x in (X (-) B) ` by XBOOLE_0:def_5; ::_thesis: verum end; begin definition let T be non empty addLoopStr ; let X, B be Subset of T; funcX (O) B -> Subset of T equals :: MATHMORP:def 4 (X (-) B) (+) B; coherence (X (-) B) (+) B is Subset of T ; end; :: deftheorem defines (O) MATHMORP:def_4_:_ for T being non empty addLoopStr for X, B being Subset of T holds X (O) B = (X (-) B) (+) B; definition let T be non empty addLoopStr ; let X, B be Subset of T; funcX (o) B -> Subset of T equals :: MATHMORP:def 5 (X (+) B) (-) B; coherence (X (+) B) (-) B is Subset of T ; end; :: deftheorem defines (o) MATHMORP:def_5_:_ for T being non empty addLoopStr for X, B being Subset of T holds X (o) B = (X (+) B) (-) B; theorem :: MATHMORP:39 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B let X, B be Subset of T; ::_thesis: ((X `) (O) (B !)) ` = X (o) B ((X `) (O) (B !)) ` = (((((X `) (-) (B !)) `) (-) B) `) ` by Th37 .= (X (+) ((B !) !)) (-) B by Th37 .= (X (+) B) (-) B by Th1 ; hence ((X `) (O) (B !)) ` = X (o) B ; ::_thesis: verum end; theorem :: MATHMORP:40 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B let X, B be Subset of T; ::_thesis: ((X `) (o) (B !)) ` = X (O) B ((X `) (o) (B !)) ` = (((X `) (+) (B !)) `) (+) ((B !) !) by Th38 .= (((X `) (+) (B !)) `) (+) B by Th1 .= (((X (-) B) `) `) (+) B by Th38 ; hence ((X `) (o) (B !)) ` = X (O) B ; ::_thesis: verum end; theorem Th41: :: MATHMORP:41 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ( X (O) B c= X & X c= X (o) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ( X (O) B c= X & X c= X (o) B ) let X, B be Subset of T; ::_thesis: ( X (O) B c= X & X c= X (o) B ) thus X (O) B c= X ::_thesis: X c= X (o) B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in X ) assume x in X (O) B ; ::_thesis: x in X then consider y1, y2 being Point of T such that A1: x = y1 + y2 and A2: y1 in X (-) B and A3: y2 in B ; consider y being Point of T such that A4: y1 = y and A5: B + y c= X by A2; x in B + y by A1, A3, A4; hence x in X by A5; ::_thesis: verum end; thus X c= X (o) B by Th20; ::_thesis: verum end; theorem Th42: :: MATHMORP:42 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T holds X (O) X = X proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (O) X = X let X be Subset of T; ::_thesis: X (O) X = X thus X (O) X c= X by Th41; :: according to XBOOLE_0:def_10 ::_thesis: X c= X (O) X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (O) X ) assume A1: x in X ; ::_thesis: x in X (O) X then reconsider x1 = x as Point of T ; X + (0. T) c= X by Th21; then 0. T in X (-) X ; then x1 + (0. T) in (X (-) X) (+) X by A1; hence x in X (O) X by RLVECT_1:4; ::_thesis: verum end; theorem :: MATHMORP:43 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) let X, B be Subset of T; ::_thesis: ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) X (O) B c= X by Th41; hence ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) by Th9; ::_thesis: verum end; theorem :: MATHMORP:44 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) let X, B be Subset of T; ::_thesis: ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) X c= X (o) B by Th41; hence ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) by Th9; ::_thesis: verum end; theorem Th45: :: MATHMORP:45 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y, B being Subset of T st X c= Y holds ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T st X c= Y holds ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) let X, Y, B be Subset of T; ::_thesis: ( X c= Y implies ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) ) assume A1: X c= Y ; ::_thesis: ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) thus X (O) B c= Y (O) B ::_thesis: X (o) B c= Y (o) B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in Y (O) B ) assume x in X (O) B ; ::_thesis: x in Y (O) B then consider x2, b2 being Point of T such that A2: x = x2 + b2 and A3: x2 in X (-) B and A4: b2 in B ; consider y being Point of T such that A5: x2 = y and A6: B + y c= X by A3; B + y c= Y by A1, A6, XBOOLE_1:1; then x2 in { y1 where y1 is Point of T : B + y1 c= Y } by A5; hence x in Y (O) B by A2, A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (o) B or x in Y (o) B ) assume x in X (o) B ; ::_thesis: x in Y (o) B then consider x2 being Point of T such that A7: x = x2 and A8: B + x2 c= X (+) B ; X (+) B c= Y (+) B by A1, Th9; then B + x2 c= Y (+) B by A8, XBOOLE_1:1; hence x in Y (o) B by A7; ::_thesis: verum end; theorem Th46: :: MATHMORP:46 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p let p be Point of T; ::_thesis: (X + p) (O) Y = (X (O) Y) + p thus (X + p) (O) Y = ((X (-) Y) + p) (+) Y by Th14 .= (X (O) Y) + p by Th15 ; ::_thesis: verum end; theorem :: MATHMORP:47 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p let p be Point of T; ::_thesis: (X + p) (o) Y = (X (o) Y) + p thus (X + p) (o) Y = ((X (+) Y) + p) (-) Y by Th15 .= (X (o) Y) + p by Th14 ; ::_thesis: verum end; theorem :: MATHMORP:48 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for C, B, X being Subset of T st C c= B holds X (O) B c= (X (-) C) (+) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for C, B, X being Subset of T st C c= B holds X (O) B c= (X (-) C) (+) B let C, B, X be Subset of T; ::_thesis: ( C c= B implies X (O) B c= (X (-) C) (+) B ) assume A1: C c= B ; ::_thesis: X (O) B c= (X (-) C) (+) B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in (X (-) C) (+) B ) assume x in X (O) B ; ::_thesis: x in (X (-) C) (+) B then consider x1, b1 being Point of T such that A2: x = x1 + b1 and A3: x1 in X (-) B and A4: b1 in B ; consider x2 being Point of T such that A5: x1 = x2 and A6: B + x2 c= X by A3; C + x2 c= B + x2 by A1, Th3; then C + x2 c= X by A6, XBOOLE_1:1; then x1 in X (-) C by A5; hence x in (X (-) C) (+) B by A2, A4; ::_thesis: verum end; theorem :: MATHMORP:49 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, C, X being Subset of T st B c= C holds X (o) B c= (X (+) C) (-) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C, X being Subset of T st B c= C holds X (o) B c= (X (+) C) (-) B let B, C, X be Subset of T; ::_thesis: ( B c= C implies X (o) B c= (X (+) C) (-) B ) assume B c= C ; ::_thesis: X (o) B c= (X (+) C) (-) B then A1: X (+) B c= X (+) C by Th10; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (o) B or x in (X (+) C) (-) B ) assume x in X (o) B ; ::_thesis: x in (X (+) C) (-) B then consider x2 being Point of T such that A2: x = x2 and A3: B + x2 c= X (+) B ; B + x2 c= X (+) C by A3, A1, XBOOLE_1:1; hence x in (X (+) C) (-) B by A2; ::_thesis: verum end; theorem Th50: :: MATHMORP:50 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T holds ( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds ( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y ) let X, Y be Subset of T; ::_thesis: ( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y ) (X (o) Y) (+) Y = (X (+) Y) (O) Y ; then A1: (X (o) Y) (+) Y c= X (+) Y by Th41; X c= X (o) Y by Th41; then X (+) Y c= (X (o) Y) (+) Y by Th9; hence X (+) Y = (X (o) Y) (+) Y by A1, XBOOLE_0:def_10; ::_thesis: X (-) Y = (X (O) Y) (-) Y (X (O) Y) (-) Y = (X (-) Y) (o) Y ; hence X (-) Y c= (X (O) Y) (-) Y by Th41; :: according to XBOOLE_0:def_10 ::_thesis: (X (O) Y) (-) Y c= X (-) Y X (O) Y c= X by Th41; hence (X (O) Y) (-) Y c= X (-) Y by Th9; ::_thesis: verum end; theorem :: MATHMORP:51 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, Y being Subset of T holds ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y ) proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y ) let X, Y be Subset of T; ::_thesis: ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y ) (X (+) Y) (O) Y = (X (o) Y) (+) Y ; hence X (+) Y = (X (+) Y) (O) Y by Th50; ::_thesis: X (-) Y = (X (-) Y) (o) Y (X (-) Y) (o) Y = (X (O) Y) (-) Y ; hence X (-) Y = (X (-) Y) (o) Y by Th50; ::_thesis: verum end; theorem :: MATHMORP:52 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds (X (O) B) (O) B = X (O) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (O) B) (O) B = X (O) B let X, B be Subset of T; ::_thesis: (X (O) B) (O) B = X (O) B thus (X (O) B) (O) B c= X (O) B by Th41; :: according to XBOOLE_0:def_10 ::_thesis: X (O) B c= (X (O) B) (O) B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in (X (O) B) (O) B ) assume x in X (O) B ; ::_thesis: x in (X (O) B) (O) B then consider x1, b1 being Point of T such that A1: x = x1 + b1 and A2: x1 in X (-) B and A3: b1 in B ; consider x2 being Point of T such that A4: x1 = x2 and A5: B + x2 c= X by A2; (B + x2) (O) B c= X (O) B by A5, Th45; then (B (O) B) + x2 c= X (O) B by Th46; then B + x2 c= X (O) B by Th42; then x1 in { x4 where x4 is Point of T : B + x4 c= X (O) B } by A4; hence x in (X (O) B) (O) B by A1, A3; ::_thesis: verum end; theorem :: MATHMORP:53 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50; theorem :: MATHMORP:54 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B let X, B, Y be Subset of T; ::_thesis: X (O) B c= (X \/ Y) (O) B X c= X \/ Y by XBOOLE_1:7; hence X (O) B c= (X \/ Y) (O) B by Th45; ::_thesis: verum end; theorem :: MATHMORP:55 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for B, B1, X being Subset of T st B = B (O) B1 holds X (O) B c= X (O) B1 proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, B1, X being Subset of T st B = B (O) B1 holds X (O) B c= X (O) B1 let B, B1, X be Subset of T; ::_thesis: ( B = B (O) B1 implies X (O) B c= X (O) B1 ) assume A1: B = B (O) B1 ; ::_thesis: X (O) B c= X (O) B1 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in X (O) B1 ) assume x in X (O) B ; ::_thesis: x in X (O) B1 then consider x1, b1 being Point of T such that A2: x = x1 + b1 and A3: x1 in X (-) B and A4: b1 in B ; consider x2 being Point of T such that A5: ( x1 = x2 & B + x2 c= X ) by A3; consider x3, b2 being Point of T such that A6: b1 = x3 + b2 and A7: x3 in B (-) B1 and A8: b2 in B1 by A1, A4; consider x4 being Point of T such that A9: x3 = x4 and A10: B1 + x4 c= B by A7; (B1 + x4) + x2 c= B + x2 by A10, Th3; then (B1 + x3) + x1 c= X by A5, A9, XBOOLE_1:1; then B1 + (x3 + x1) c= X by Th16; then x1 + x3 in X (-) B1 ; then (x1 + x3) + b2 in (X (-) B1) (+) B1 by A8; hence x in X (O) B1 by A2, A6, RLVECT_1:def_3; ::_thesis: verum end; begin definition let t be real number ; let T be non empty RLSStruct ; let A be Subset of T; funct (.) A -> Subset of T equals :: MATHMORP:def 6 { (t * a) where a is Point of T : a in A } ; coherence { (t * a) where a is Point of T : a in A } is Subset of T proof now__::_thesis:_for_x_being_set_st_x_in__{__(t_*_a)_where_a_is_Point_of_T_:_a_in_A__}__holds_ x_in_the_carrier_of_T let x be set ; ::_thesis: ( x in { (t * a) where a is Point of T : a in A } implies x in the carrier of T ) assume x in { (t * a) where a is Point of T : a in A } ; ::_thesis: x in the carrier of T then ex q being Point of T st ( x = t * q & q in A ) ; hence x in the carrier of T ; ::_thesis: verum end; hence { (t * a) where a is Point of T : a in A } is Subset of T by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines (.) MATHMORP:def_6_:_ for t being real number for T being non empty RLSStruct for A being Subset of T holds t (.) A = { (t * a) where a is Point of T : a in A } ; theorem :: MATHMORP:56 for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct for X being Subset of T st X = {} holds 0 (.) X = {} proof let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T st X = {} holds 0 (.) X = {} let X be Subset of T; ::_thesis: ( X = {} implies 0 (.) X = {} ) assume A1: X = {} ; ::_thesis: 0 (.) X = {} now__::_thesis:_for_x_being_set_holds_not_x_in_0_(.)_X given x being set such that A2: x in 0 (.) X ; ::_thesis: contradiction ex a being Point of T st ( x = 0 * a & a in X ) by A2; hence contradiction by A1; ::_thesis: verum end; hence 0 (.) X = {} by XBOOLE_0:def_1; ::_thesis: verum end; theorem :: MATHMORP:57 for n being Element of NAT for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))} proof let n be Element of NAT ; ::_thesis: for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))} set T = TOP-REAL n; let X be non empty Subset of (TOP-REAL n); ::_thesis: 0 (.) X = {(0. (TOP-REAL n))} thus 0 (.) X c= {(0. (TOP-REAL n))} :: according to XBOOLE_0:def_10 ::_thesis: {(0. (TOP-REAL n))} c= 0 (.) X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 0 (.) X or x in {(0. (TOP-REAL n))} ) assume x in 0 (.) X ; ::_thesis: x in {(0. (TOP-REAL n))} then ex a being Point of (TOP-REAL n) st ( x = 0 * a & a in X ) ; then x = 0. (TOP-REAL n) by EUCLID:29; hence x in {(0. (TOP-REAL n))} by ZFMISC_1:31; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (TOP-REAL n))} or x in 0 (.) X ) set d = the Element of X; reconsider d1 = the Element of X as Point of (TOP-REAL n) ; assume x in {(0. (TOP-REAL n))} ; ::_thesis: x in 0 (.) X then {x} c= {(0. (TOP-REAL n))} by ZFMISC_1:31; then x = 0. (TOP-REAL n) by ZFMISC_1:18; then x = 0 * d1 by EUCLID:29; hence x in 0 (.) X ; ::_thesis: verum end; theorem Th58: :: MATHMORP:58 for n being Element of NAT for X being Subset of (TOP-REAL n) holds 1 (.) X = X proof let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds 1 (.) X = X let X be Subset of (TOP-REAL n); ::_thesis: 1 (.) X = X thus 1 (.) X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= 1 (.) X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 (.) X or x in X ) assume x in 1 (.) X ; ::_thesis: x in X then ex z being Point of (TOP-REAL n) st ( x = 1 * z & z in X ) ; hence x in X by EUCLID:29; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in 1 (.) X ) assume A1: x in X ; ::_thesis: x in 1 (.) X then reconsider x1 = x as Point of (TOP-REAL n) ; x1 = 1 * x1 by EUCLID:29; hence x in 1 (.) X by A1; ::_thesis: verum end; theorem :: MATHMORP:59 for n being Element of NAT for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X proof let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X let X be Subset of (TOP-REAL n); ::_thesis: 2 (.) X c= X (+) X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 2 (.) X or x in X (+) X ) assume x in 2 (.) X ; ::_thesis: x in X (+) X then consider z being Point of (TOP-REAL n) such that A1: x = 2 * z and A2: z in X ; x = (1 + 1) * z by A1 .= (1 * z) + (1 * z) by EUCLID:33 .= z + (1 * z) by EUCLID:29 .= z + z by EUCLID:29 ; hence x in X (+) X by A2; ::_thesis: verum end; theorem Th60: :: MATHMORP:60 for t, s being real number for n being Element of NAT for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X) proof let t, s be real number ; ::_thesis: for n being Element of NAT for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X) let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X) let X be Subset of (TOP-REAL n); ::_thesis: (t * s) (.) X = t (.) (s (.) X) thus (t * s) (.) X c= t (.) (s (.) X) :: according to XBOOLE_0:def_10 ::_thesis: t (.) (s (.) X) c= (t * s) (.) X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (t * s) (.) X or x in t (.) (s (.) X) ) assume x in (t * s) (.) X ; ::_thesis: x in t (.) (s (.) X) then consider z being Point of (TOP-REAL n) such that A1: ( x = (t * s) * z & z in X ) ; ( x = t * (s * z) & s * z in s (.) X ) by A1, EUCLID:30; hence x in t (.) (s (.) X) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t (.) (s (.) X) or x in (t * s) (.) X ) assume x in t (.) (s (.) X) ; ::_thesis: x in (t * s) (.) X then consider z being Point of (TOP-REAL n) such that A2: x = t * z and A3: z in s (.) X ; consider z1 being Point of (TOP-REAL n) such that A4: z = s * z1 and A5: z1 in X by A3; x = (t * s) * z1 by A2, A4, EUCLID:30; hence x in (t * s) (.) X by A5; ::_thesis: verum end; theorem Th61: :: MATHMORP:61 for t being real number for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st X c= Y holds t (.) X c= t (.) Y proof let t be real number ; ::_thesis: for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st X c= Y holds t (.) X c= t (.) Y let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st X c= Y holds t (.) X c= t (.) Y let X, Y be Subset of (TOP-REAL n); ::_thesis: ( X c= Y implies t (.) X c= t (.) Y ) assume A1: X c= Y ; ::_thesis: t (.) X c= t (.) Y let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t (.) X or x in t (.) Y ) assume x in t (.) X ; ::_thesis: x in t (.) Y then ex a being Point of (TOP-REAL n) st ( x = t * a & a in X ) ; hence x in t (.) Y by A1; ::_thesis: verum end; theorem Th62: :: MATHMORP:62 for t being real number for n being Element of NAT for X being Subset of (TOP-REAL n) for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x) proof let t be real number ; ::_thesis: for n being Element of NAT for X being Subset of (TOP-REAL n) for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x) let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x) let X be Subset of (TOP-REAL n); ::_thesis: for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x) let x be Point of (TOP-REAL n); ::_thesis: t (.) (X + x) = (t (.) X) + (t * x) thus t (.) (X + x) c= (t (.) X) + (t * x) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) + (t * x) c= t (.) (X + x) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X + x) or b in (t (.) X) + (t * x) ) assume b in t (.) (X + x) ; ::_thesis: b in (t (.) X) + (t * x) then consider a being Point of (TOP-REAL n) such that A1: b = t * a and A2: a in X + x ; consider x1 being Point of (TOP-REAL n) such that A3: a = x1 + x and A4: x1 in X by A2; A5: t * x1 in t (.) X by A4; b = (t * x1) + (t * x) by A1, A3, EUCLID:32; hence b in (t (.) X) + (t * x) by A5; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) + (t * x) or b in t (.) (X + x) ) assume b in (t (.) X) + (t * x) ; ::_thesis: b in t (.) (X + x) then consider x1 being Point of (TOP-REAL n) such that A6: b = x1 + (t * x) and A7: x1 in t (.) X ; consider a being Point of (TOP-REAL n) such that A8: x1 = t * a and A9: a in X by A7; A10: a + x in X + x by A9; b = t * (a + x) by A6, A8, EUCLID:32; hence b in t (.) (X + x) by A10; ::_thesis: verum end; theorem Th63: :: MATHMORP:63 for t being real number for n being Element of NAT for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y) proof let t be real number ; ::_thesis: for n being Element of NAT for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y) let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y) let X, Y be Subset of (TOP-REAL n); ::_thesis: t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y) thus t (.) (X (+) Y) c= (t (.) X) (+) (t (.) Y) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) (+) (t (.) Y) c= t (.) (X (+) Y) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X (+) Y) or b in (t (.) X) (+) (t (.) Y) ) assume b in t (.) (X (+) Y) ; ::_thesis: b in (t (.) X) (+) (t (.) Y) then consider a being Point of (TOP-REAL n) such that A1: b = t * a and A2: a in X (+) Y ; consider x, y being Point of (TOP-REAL n) such that A3: a = x + y and A4: ( x in X & y in Y ) by A2; A5: ( t * x in t (.) X & t * y in t (.) Y ) by A4; b = (t * x) + (t * y) by A1, A3, EUCLID:32; hence b in (t (.) X) (+) (t (.) Y) by A5; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) (+) (t (.) Y) or b in t (.) (X (+) Y) ) assume b in (t (.) X) (+) (t (.) Y) ; ::_thesis: b in t (.) (X (+) Y) then consider x, y being Point of (TOP-REAL n) such that A6: b = x + y and A7: x in t (.) X and A8: y in t (.) Y ; consider y1 being Point of (TOP-REAL n) such that A9: y = t * y1 and A10: y1 in Y by A8; consider x1 being Point of (TOP-REAL n) such that A11: x = t * x1 and A12: x1 in X by A7; A13: x1 + y1 in X (+) Y by A12, A10; b = t * (x1 + y1) by A6, A11, A9, EUCLID:32; hence b in t (.) (X (+) Y) by A13; ::_thesis: verum end; theorem Th64: :: MATHMORP:64 for t being real number for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) proof let t be real number ; ::_thesis: for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) ) assume A1: t <> 0 ; ::_thesis: t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) thus t (.) (X (-) Y) c= (t (.) X) (-) (t (.) Y) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) (-) (t (.) Y) c= t (.) (X (-) Y) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X (-) Y) or b in (t (.) X) (-) (t (.) Y) ) assume b in t (.) (X (-) Y) ; ::_thesis: b in (t (.) X) (-) (t (.) Y) then consider a being Point of (TOP-REAL n) such that A2: b = t * a and A3: a in X (-) Y ; consider x being Point of (TOP-REAL n) such that A4: a = x and A5: Y + x c= X by A3; t (.) (Y + x) c= t (.) X by A5, Th61; then (t (.) Y) + (t * x) c= t (.) X by Th62; hence b in (t (.) X) (-) (t (.) Y) by A2, A4; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) (-) (t (.) Y) or b in t (.) (X (-) Y) ) assume b in (t (.) X) (-) (t (.) Y) ; ::_thesis: b in t (.) (X (-) Y) then consider x being Point of (TOP-REAL n) such that A6: b = x and A7: (t (.) Y) + x c= t (.) X ; (1 / t) (.) ((t (.) Y) + x) c= (1 / t) (.) (t (.) X) by A7, Th61; then (1 / t) (.) ((t (.) Y) + x) c= ((1 / t) * t) (.) X by Th60; then ((1 / t) (.) (t (.) Y)) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th62; then (((1 / t) * t) (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th60; then (1 (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by A1, XCMPLX_1:87; then (1 (.) Y) + ((1 / t) * x) c= 1 (.) X by A1, XCMPLX_1:87; then Y + ((1 / t) * x) c= 1 (.) X by Th58; then Y + ((1 / t) * x) c= X by Th58; then (1 / t) * x in { z where z is Point of (TOP-REAL n) : Y + z c= X } ; then t * ((1 / t) * x) in { (t * a1) where a1 is Point of (TOP-REAL n) : a1 in X (-) Y } ; then ((1 / t) * t) * x in t (.) (X (-) Y) by EUCLID:30; then 1 * x in t (.) (X (-) Y) by A1, XCMPLX_1:87; hence b in t (.) (X (-) Y) by A6, EUCLID:29; ::_thesis: verum end; theorem :: MATHMORP:65 for t being real number for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) proof let t be real number ; ::_thesis: for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) ) assume A1: t <> 0 ; ::_thesis: t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) t (.) (X (O) Y) = (t (.) (X (-) Y)) (+) (t (.) Y) by Th63 .= ((t (.) X) (-) (t (.) Y)) (+) (t (.) Y) by A1, Th64 ; hence t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) ; ::_thesis: verum end; theorem :: MATHMORP:66 for t being real number for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) proof let t be real number ; ::_thesis: for n being Element of NAT for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) ) assume t <> 0 ; ::_thesis: t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) then t (.) (X (o) Y) = (t (.) (X (+) Y)) (-) (t (.) Y) by Th64 .= ((t (.) X) (+) (t (.) Y)) (-) (t (.) Y) by Th63 ; hence t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) ; ::_thesis: verum end; begin definition let T be non empty RLSStruct ; let X, B1, B2 be Subset of T; funcX (*) (B1,B2) -> Subset of T equals :: MATHMORP:def 7 (X (-) B1) /\ ((X `) (-) B2); coherence (X (-) B1) /\ ((X `) (-) B2) is Subset of T ; end; :: deftheorem defines (*) MATHMORP:def_7_:_ for T being non empty RLSStruct for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2); definition let T be non empty RLSStruct ; let X, B1, B2 be Subset of T; funcX (&) (B1,B2) -> Subset of T equals :: MATHMORP:def 8 X \/ (X (*) (B1,B2)); coherence X \/ (X (*) (B1,B2)) is Subset of T ; end; :: deftheorem defines (&) MATHMORP:def_8_:_ for T being non empty RLSStruct for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2)); definition let T be non empty RLSStruct ; let X, B1, B2 be Subset of T; funcX (@) (B1,B2) -> Subset of T equals :: MATHMORP:def 9 X \ (X (*) (B1,B2)); coherence X \ (X (*) (B1,B2)) is Subset of T ; end; :: deftheorem defines (@) MATHMORP:def_9_:_ for T being non empty RLSStruct for X, B1, B2 being Subset of T holds X (@) (B1,B2) = X \ (X (*) (B1,B2)); theorem :: MATHMORP:67 for n being Element of NAT for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds X (*) (B1,B2) = (X `) (-) B2 proof let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds X (*) (B1,B2) = (X `) (-) B2 let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( B1 = {} implies X (*) (B1,B2) = (X `) (-) B2 ) assume B1 = {} ; ::_thesis: X (*) (B1,B2) = (X `) (-) B2 then X (*) (B1,B2) = ((X `) (-) B2) /\ the carrier of (TOP-REAL n) by Th8; hence X (*) (B1,B2) = (X `) (-) B2 by XBOOLE_1:28; ::_thesis: verum end; theorem :: MATHMORP:68 for n being Element of NAT for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds X (*) (B1,B2) = X (-) B1 proof let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds X (*) (B1,B2) = X (-) B1 let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( B2 = {} implies X (*) (B1,B2) = X (-) B1 ) assume B2 = {} ; ::_thesis: X (*) (B1,B2) = X (-) B1 then X (*) (B1,B2) = (X (-) B1) /\ the carrier of (TOP-REAL n) by Th8; hence X (*) (B1,B2) = X (-) B1 by XBOOLE_1:28; ::_thesis: verum end; theorem :: MATHMORP:69 for n being Element of NAT for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds X (*) (B1,B2) c= X proof let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds X (*) (B1,B2) c= X let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B1 implies X (*) (B1,B2) c= X ) assume A1: 0. (TOP-REAL n) in B1 ; ::_thesis: X (*) (B1,B2) c= X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (*) (B1,B2) or x in X ) assume x in X (*) (B1,B2) ; ::_thesis: x in X then x in X (-) B1 by XBOOLE_0:def_4; then consider y being Point of (TOP-REAL n) such that A2: x = y and A3: B1 + y c= X ; (0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B1 } by A1; then x in B1 + y by A2, RLVECT_1:4; hence x in X by A3; ::_thesis: verum end; theorem :: MATHMORP:70 for n being Element of NAT for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds (X (*) (B1,B2)) /\ X = {} proof let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds (X (*) (B1,B2)) /\ X = {} let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B2 implies (X (*) (B1,B2)) /\ X = {} ) assume A1: 0. (TOP-REAL n) in B2 ; ::_thesis: (X (*) (B1,B2)) /\ X = {} now__::_thesis:_for_x_being_set_holds_not_x_in_(X_(*)_(B1,B2))_/\_X given x being set such that A2: x in (X (*) (B1,B2)) /\ X ; ::_thesis: contradiction A3: x in X by A2, XBOOLE_0:def_4; x in X (*) (B1,B2) by A2, XBOOLE_0:def_4; then x in (X `) (-) B2 by XBOOLE_0:def_4; then consider y being Point of (TOP-REAL n) such that A4: x = y and A5: B2 + y c= X ` ; (0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B2 } by A1; then x in B2 + y by A4, RLVECT_1:4; hence contradiction by A3, A5, XBOOLE_0:def_5; ::_thesis: verum end; hence (X (*) (B1,B2)) /\ X = {} by XBOOLE_0:def_1; ::_thesis: verum end; theorem :: MATHMORP:71 for n being Element of NAT for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds X (&) (B1,B2) = X proof let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds X (&) (B1,B2) = X let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B1 implies X (&) (B1,B2) = X ) assume A1: 0. (TOP-REAL n) in B1 ; ::_thesis: X (&) (B1,B2) = X thus X (&) (B1,B2) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (&) (B1,B2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (&) (B1,B2) or x in X ) assume A2: x in X (&) (B1,B2) ; ::_thesis: x in X percases ( x in X or x in X (*) (B1,B2) ) by A2, XBOOLE_0:def_3; suppose x in X ; ::_thesis: x in X hence x in X ; ::_thesis: verum end; suppose x in X (*) (B1,B2) ; ::_thesis: x in X then x in X (-) B1 by XBOOLE_0:def_4; then consider y being Point of (TOP-REAL n) such that A3: x = y and A4: B1 + y c= X ; (0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B1 } by A1; then x in B1 + y by A3, RLVECT_1:4; hence x in X by A4; ::_thesis: verum end; end; end; thus X c= X (&) (B1,B2) by XBOOLE_1:7; ::_thesis: verum end; theorem :: MATHMORP:72 for n being Element of NAT for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds X (@) (B1,B2) = X proof let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds X (@) (B1,B2) = X let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B2 implies X (@) (B1,B2) = X ) assume A1: 0. (TOP-REAL n) in B2 ; ::_thesis: X (@) (B1,B2) = X thus X (@) (B1,B2) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (@) (B1,B2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (@) (B1,B2) or x in X ) assume x in X (@) (B1,B2) ; ::_thesis: x in X hence x in X by XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (@) (B1,B2) ) assume A2: x in X ; ::_thesis: x in X (@) (B1,B2) not x in X (*) (B1,B2) proof assume x in X (*) (B1,B2) ; ::_thesis: contradiction then x in (X `) (-) B2 by XBOOLE_0:def_4; then consider y being Point of (TOP-REAL n) such that A3: x = y and A4: B2 + y c= X ` ; (0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B2 } by A1; then x in B2 + y by A3, RLVECT_1:4; hence contradiction by A2, A4, XBOOLE_0:def_5; ::_thesis: verum end; hence x in X (@) (B1,B2) by A2, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: MATHMORP:73 for n being Element of NAT for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) ` proof let n be Element of NAT ; ::_thesis: for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) ` let X, B2, B1 be Subset of (TOP-REAL n); ::_thesis: X (@) (B2,B1) = ((X `) (&) (B1,B2)) ` ((X `) (&) (B1,B2)) ` = ((X \ (((X `) (-) B1) /\ (((X `) `) (-) B2))) `) ` by SUBSET_1:14 .= X \ (X (*) (B2,B1)) ; hence X (@) (B2,B1) = ((X `) (&) (B1,B2)) ` ; ::_thesis: verum end; begin theorem Th74: :: MATHMORP:74 for V being RealLinearSpace for B being Subset of V holds ( B is convex iff for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) proof let V be RealLinearSpace; ::_thesis: for B being Subset of V holds ( B is convex iff for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) let B be Subset of V; ::_thesis: ( B is convex iff for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) thus ( B is convex implies for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) ::_thesis: ( ( for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) implies B is convex ) proof assume A1: B is convex ; ::_thesis: for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B proof let x, y be Point of V; ::_thesis: for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in B & y in B implies (r * x) + ((1 - r) * y) in B ) assume that A2: ( 0 <= r & r <= 1 ) and A3: ( x in B & y in B ) ; ::_thesis: (r * x) + ((1 - r) * y) in B r is Real by XREAL_0:def_1; then ((1 - r) * y) + (r * x) in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A2; then A4: ((1 - r) * y) + (r * x) in LSeg (x,y) by RLTOPSP1:def_2; LSeg (x,y) c= B by A1, A3, JORDAN1:def_1; hence (r * x) + ((1 - r) * y) in B by A4; ::_thesis: verum end; hence for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ; ::_thesis: verum end; ( ( for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) implies B is convex ) proof assume A5: for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ; ::_thesis: B is convex for x, y being Point of V st x in B & y in B holds LSeg (x,y) c= B proof let x, y be Point of V; ::_thesis: ( x in B & y in B implies LSeg (x,y) c= B ) assume A6: ( x in B & y in B ) ; ::_thesis: LSeg (x,y) c= B let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in LSeg (x,y) or p in B ) assume p in LSeg (x,y) ; ::_thesis: p in B then p in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RLTOPSP1:def_2; then ex r1 being Real st ( p = ((1 - r1) * y) + (r1 * x) & 0 <= r1 & r1 <= 1 ) ; hence p in B by A5, A6; ::_thesis: verum end; hence B is convex by RLTOPSP1:22; ::_thesis: verum end; hence ( ( for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) implies B is convex ) ; ::_thesis: verum end; definition let V be RealLinearSpace; let B be Subset of V; redefine attr B is convex means :Def10: :: MATHMORP:def 10 for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B; compatibility ( B is convex iff for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ) by Th74; end; :: deftheorem Def10 defines convex MATHMORP:def_10_:_ for V being RealLinearSpace for B being Subset of V holds ( B is convex iff for x, y being Point of V for r being real number st 0 <= r & r <= 1 & x in B & y in B holds (r * x) + ((1 - r) * y) in B ); theorem :: MATHMORP:75 for n being Element of NAT for X being Subset of (TOP-REAL n) st X is convex holds X ! is convex proof let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) st X is convex holds X ! is convex let X be Subset of (TOP-REAL n); ::_thesis: ( X is convex implies X ! is convex ) assume A1: X is convex ; ::_thesis: X ! is convex for x, y being Point of (TOP-REAL n) for r being real number st 0 <= r & r <= 1 & x in X ! & y in X ! holds (r * x) + ((1 - r) * y) in X ! proof let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X ! & y in X ! holds (r * x) + ((1 - r) * y) in X ! let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X ! & y in X ! implies (r * x) + ((1 - r) * y) in X ! ) assume that A2: ( 0 <= r & r <= 1 ) and A3: x in X ! and A4: y in X ! ; ::_thesis: (r * x) + ((1 - r) * y) in X ! consider x2 being Point of (TOP-REAL n) such that A5: y = - x2 and A6: x2 in X by A4; consider x1 being Point of (TOP-REAL n) such that A7: x = - x1 and A8: x1 in X by A3; (r * x1) + ((1 - r) * x2) in X by A1, A2, A8, A6, Def10; then - ((r * x1) + ((1 - r) * x2)) in X ! ; then (- (r * x1)) - ((1 - r) * x2) in X ! by EUCLID:38; then (r * (- x1)) + (- ((1 - r) * x2)) in X ! by EUCLID:40; hence (r * x) + ((1 - r) * y) in X ! by A7, A5, EUCLID:40; ::_thesis: verum end; hence X ! is convex by Def10; ::_thesis: verum end; theorem Th76: :: MATHMORP:76 for n being Element of NAT for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds ( X (+) B is convex & X (-) B is convex ) proof let n be Element of NAT ; ::_thesis: for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds ( X (+) B is convex & X (-) B is convex ) let X, B be Subset of (TOP-REAL n); ::_thesis: ( X is convex & B is convex implies ( X (+) B is convex & X (-) B is convex ) ) assume that A1: X is convex and A2: B is convex ; ::_thesis: ( X (+) B is convex & X (-) B is convex ) for x, y being Point of (TOP-REAL n) for r being real number st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds (r * x) + ((1 - r) * y) in X (+) B proof let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds (r * x) + ((1 - r) * y) in X (+) B let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X (+) B & y in X (+) B implies (r * x) + ((1 - r) * y) in X (+) B ) assume that A3: ( 0 <= r & r <= 1 ) and A4: x in X (+) B and A5: y in X (+) B ; ::_thesis: (r * x) + ((1 - r) * y) in X (+) B consider x2, b2 being Point of (TOP-REAL n) such that A6: y = x2 + b2 and A7: ( x2 in X & b2 in B ) by A5; consider x1, b1 being Point of (TOP-REAL n) such that A8: x = x1 + b1 and A9: ( x1 in X & b1 in B ) by A4; ( (r * x1) + ((1 - r) * x2) in X & (r * b1) + ((1 - r) * b2) in B ) by A1, A2, A3, A9, A7, Def10; then ((r * x1) + ((1 - r) * x2)) + ((r * b1) + ((1 - r) * b2)) in { (x3 + b3) where x3, b3 is Point of (TOP-REAL n) : ( x3 in X & b3 in B ) } ; then (((r * x1) + ((1 - r) * x2)) + (r * b1)) + ((1 - r) * b2) in X (+) B by EUCLID:26; then (((r * x1) + (r * b1)) + ((1 - r) * x2)) + ((1 - r) * b2) in X (+) B by EUCLID:26; then ((r * x1) + (r * b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by EUCLID:26; then (r * (x1 + b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by EUCLID:32; hence (r * x) + ((1 - r) * y) in X (+) B by A8, A6, EUCLID:32; ::_thesis: verum end; hence X (+) B is convex by Def10; ::_thesis: X (-) B is convex for x, y being Point of (TOP-REAL n) for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds (r * x) + ((1 - r) * y) in X (-) B proof let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds (r * x) + ((1 - r) * y) in X (-) B let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X (-) B & y in X (-) B implies (r * x) + ((1 - r) * y) in X (-) B ) assume that A10: ( 0 <= r & r <= 1 ) and A11: ( x in X (-) B & y in X (-) B ) ; ::_thesis: (r * x) + ((1 - r) * y) in X (-) B A12: ( ex x1 being Point of (TOP-REAL n) st ( x = x1 & B + x1 c= X ) & ex y1 being Point of (TOP-REAL n) st ( y = y1 & B + y1 c= X ) ) by A11; B + ((r * x) + ((1 - r) * y)) c= X proof let b1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not b1 in B + ((r * x) + ((1 - r) * y)) or b1 in X ) assume b1 in B + ((r * x) + ((1 - r) * y)) ; ::_thesis: b1 in X then consider b being Point of (TOP-REAL n) such that A13: b1 = b + ((r * x) + ((1 - r) * y)) and A14: b in B ; ( b + x in B + x & b + y in { (b2 + y) where b2 is Point of (TOP-REAL n) : b2 in B } ) by A14; then (r * (b + x)) + ((1 - r) * (b + y)) in X by A1, A10, A12, Def10; then ((r * b) + (r * x)) + ((1 - r) * (b + y)) in X by EUCLID:32; then ((r * b) + (r * x)) + (((1 - r) * b) + ((1 - r) * y)) in X by EUCLID:32; then (((r * b) + (r * x)) + ((1 - r) * b)) + ((1 - r) * y) in X by EUCLID:26; then (((r * b) + (r * x)) + ((1 * b) - (r * b))) + ((1 - r) * y) in X by EUCLID:50; then ((((r * b) + (r * x)) + (1 * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:45; then ((((r * x) + (1 * b)) + (r * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:26; then ((r * x) + (1 * b)) + ((1 - r) * y) in X by EUCLID:48; then (1 * b) + ((r * x) + ((1 - r) * y)) in X by EUCLID:26; hence b1 in X by A13, EUCLID:29; ::_thesis: verum end; hence (r * x) + ((1 - r) * y) in X (-) B ; ::_thesis: verum end; hence X (-) B is convex by Def10; ::_thesis: verum end; theorem :: MATHMORP:77 for n being Element of NAT for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds ( X (O) B is convex & X (o) B is convex ) proof let n be Element of NAT ; ::_thesis: for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds ( X (O) B is convex & X (o) B is convex ) let X, B be Subset of (TOP-REAL n); ::_thesis: ( X is convex & B is convex implies ( X (O) B is convex & X (o) B is convex ) ) assume that A1: X is convex and A2: B is convex ; ::_thesis: ( X (O) B is convex & X (o) B is convex ) X (-) B is convex by A1, A2, Th76; hence X (O) B is convex by A2, Th76; ::_thesis: X (o) B is convex X (+) B is convex by A1, A2, Th76; hence X (o) B is convex by A2, Th76; ::_thesis: verum end; theorem :: MATHMORP:78 for t, s being real number for n being Element of NAT for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds (s + t) (.) B = (s (.) B) (+) (t (.) B) proof let t, s be real number ; ::_thesis: for n being Element of NAT for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds (s + t) (.) B = (s (.) B) (+) (t (.) B) let n be Element of NAT ; ::_thesis: for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds (s + t) (.) B = (s (.) B) (+) (t (.) B) let B be Subset of (TOP-REAL n); ::_thesis: ( B is convex & 0 < t & 0 < s implies (s + t) (.) B = (s (.) B) (+) (t (.) B) ) assume that A1: B is convex and A2: ( 0 < t & 0 < s ) ; ::_thesis: (s + t) (.) B = (s (.) B) (+) (t (.) B) thus (s + t) (.) B c= (s (.) B) (+) (t (.) B) :: according to XBOOLE_0:def_10 ::_thesis: (s (.) B) (+) (t (.) B) c= (s + t) (.) B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (s + t) (.) B or x in (s (.) B) (+) (t (.) B) ) assume x in (s + t) (.) B ; ::_thesis: x in (s (.) B) (+) (t (.) B) then consider b being Point of (TOP-REAL n) such that A3: x = (s + t) * b and A4: b in B ; A5: t * b in t (.) B by A4; ( x = (s * b) + (t * b) & s * b in s (.) B ) by A3, A4, EUCLID:33; hence x in (s (.) B) (+) (t (.) B) by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (s (.) B) (+) (t (.) B) or x in (s + t) (.) B ) assume x in (s (.) B) (+) (t (.) B) ; ::_thesis: x in (s + t) (.) B then consider s1, s2 being Point of (TOP-REAL n) such that A6: x = s1 + s2 and A7: s1 in s (.) B and A8: s2 in t (.) B ; consider b2 being Point of (TOP-REAL n) such that A9: s2 = t * b2 and A10: b2 in B by A8; consider b1 being Point of (TOP-REAL n) such that A11: s1 = s * b1 and A12: b1 in B by A7; s / (s + t) < (s + t) / (s + t) by A2, XREAL_1:29, XREAL_1:74; then s / (s + t) < 1 by A2, XCMPLX_1:60; then ((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) in B by A1, A2, A12, A10, Def10; then (s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) in { ((s + t) * zz) where zz is Point of (TOP-REAL n) : zz in B } ; then ((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:32; then (((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:30; then (((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by EUCLID:30; then (s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:87; then (s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:60; then (s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2) in (s + t) (.) B by XCMPLX_1:120; hence x in (s + t) (.) B by A2, A6, A11, A9, XCMPLX_1:87; ::_thesis: verum end;