:: SUBSTLAT semantic presentation begin definition let V, C be set ; func SubstitutionSet (V,C) -> Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1 { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } ; coherence { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } is Subset of (Fin (PFuncs (V,C))) proof set IT = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } ; { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } c= Fin (PFuncs (V,C)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } or x in Fin (PFuncs (V,C)) ) assume x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } ; ::_thesis: x in Fin (PFuncs (V,C)) then ex B being Element of Fin (PFuncs (V,C)) st ( B = x & ( for u being set st u in B holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds s = t ) ) ; hence x in Fin (PFuncs (V,C)) ; ::_thesis: verum end; hence { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } is Subset of (Fin (PFuncs (V,C))) ; ::_thesis: verum end; end; :: deftheorem defines SubstitutionSet SUBSTLAT:def_1_:_ for V, C being set holds SubstitutionSet (V,C) = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) } ; Lm1: for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds a is finite proof let V, C be set ; ::_thesis: for a, b being set st b in SubstitutionSet (V,C) & a in b holds a is finite let a, b be set ; ::_thesis: ( b in SubstitutionSet (V,C) & a in b implies a is finite ) assume that A1: b in SubstitutionSet (V,C) and A2: a in b ; ::_thesis: a is finite ex A being Element of Fin (PFuncs (V,C)) st ( A = b & ( for u being set st u in A holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds s = t ) ) by A1; hence a is finite by A2; ::_thesis: verum end; theorem Th1: :: SUBSTLAT:1 for V, C being set holds {} in SubstitutionSet (V,C) proof let V, C be set ; ::_thesis: {} in SubstitutionSet (V,C) {} c= PFuncs (V,C) by XBOOLE_1:2; then A1: {} in Fin (PFuncs (V,C)) by FINSUB_1:def_5; ( ( for u being set st u in {} holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in {} & t in {} & s c= t holds s = t ) ) ; hence {} in SubstitutionSet (V,C) by A1; ::_thesis: verum end; theorem Th2: :: SUBSTLAT:2 for V, C being set holds {{}} in SubstitutionSet (V,C) proof let V, C be set ; ::_thesis: {{}} in SubstitutionSet (V,C) A1: for s, t being Element of PFuncs (V,C) st s in {{}} & t in {{}} & s c= t holds s = t proof let s, t be Element of PFuncs (V,C); ::_thesis: ( s in {{}} & t in {{}} & s c= t implies s = t ) assume that A2: s in {{}} and A3: t in {{}} and s c= t ; ::_thesis: s = t s = {} by A2, TARSKI:def_1; hence s = t by A3, TARSKI:def_1; ::_thesis: verum end; {} is PartFunc of V,C by RELSET_1:12; then {} in PFuncs (V,C) by PARTFUN1:45; then {{}} c= PFuncs (V,C) by ZFMISC_1:31; then A4: {{}} in Fin (PFuncs (V,C)) by FINSUB_1:def_5; for u being set st u in {{}} holds u is finite ; hence {{}} in SubstitutionSet (V,C) by A4, A1; ::_thesis: verum end; registration let V, C be set ; cluster SubstitutionSet (V,C) -> non empty ; coherence not SubstitutionSet (V,C) is empty by Th2; end; definition let V, C be set ; let A, B be Element of SubstitutionSet (V,C); :: original: \/ redefine funcA \/ B -> Element of Fin (PFuncs (V,C)); coherence A \/ B is Element of Fin (PFuncs (V,C)) proof A \/ B in Fin (PFuncs (V,C)) ; hence A \/ B is Element of Fin (PFuncs (V,C)) ; ::_thesis: verum end; end; registration let V, C be set ; cluster non empty for Element of SubstitutionSet (V,C); existence not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty proof {{}} in SubstitutionSet (V,C) by Th2; hence not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty ; ::_thesis: verum end; end; registration let V, C be set ; cluster -> finite for Element of SubstitutionSet (V,C); coherence for b1 being Element of SubstitutionSet (V,C) holds b1 is finite ; end; definition let V, C be set ; let A be Element of Fin (PFuncs (V,C)); func mi A -> Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2 { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } ; coherence { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C) proof set M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } ; A1: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } c= PFuncs (V,C) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } or a in PFuncs (V,C) ) assume a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } ; ::_thesis: a in PFuncs (V,C) then ex t9 being Element of PFuncs (V,C) st ( a = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t9 ) iff s = t9 ) ) ) ; hence a in PFuncs (V,C) ; ::_thesis: verum end; A2: now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_PFuncs_(V,C)_:_(_t_is_finite_&_(_for_s_being_Element_of_PFuncs_(V,C)_holds_ (_(_s_in_A_&_s_c=_t_)_iff_s_=_t_)_)_)__}__holds_ x_in_A let x be set ; ::_thesis: ( x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } implies x in A ) assume x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } ; ::_thesis: x in A then ex t being Element of PFuncs (V,C) st ( x = t & t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) ; hence x in A ; ::_thesis: verum end; then A3: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } c= A by TARSKI:def_3; reconsider M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } as set ; reconsider M9 = M as Element of Fin (PFuncs (V,C)) by A1, A3, FINSUB_1:def_5; A4: for u being set st u in M9 holds u is finite proof let u be set ; ::_thesis: ( u in M9 implies u is finite ) assume u in M9 ; ::_thesis: u is finite then ex t9 being Element of PFuncs (V,C) st ( u = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t9 ) iff s = t9 ) ) ) ; hence u is finite ; ::_thesis: verum end; for s, t being Element of PFuncs (V,C) st s in M9 & t in M9 & s c= t holds s = t proof let s, t be Element of PFuncs (V,C); ::_thesis: ( s in M9 & t in M9 & s c= t implies s = t ) assume that A5: ( s in M9 & t in M9 ) and A6: s c= t ; ::_thesis: s = t ( s in A & ex tt being Element of PFuncs (V,C) st ( t = tt & tt is finite & ( for ss being Element of PFuncs (V,C) holds ( ( ss in A & ss c= tt ) iff ss = tt ) ) ) ) by A2, A5; hence s = t by A6; ::_thesis: verum end; then M in { A1 where A1 is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A1 holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds s = t ) ) } by A4; hence { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C) ; ::_thesis: verum end; end; :: deftheorem defines mi SUBSTLAT:def_2_:_ for V, C being set for A being Element of Fin (PFuncs (V,C)) holds mi A = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in A & s c= t ) iff s = t ) ) ) } ; registration let V, C be set ; cluster -> functional for Element of SubstitutionSet (V,C); coherence for b1 being Element of SubstitutionSet (V,C) holds b1 is functional proof let A be Element of SubstitutionSet (V,C); ::_thesis: A is functional A c= PFuncs (V,C) by FINSUB_1:def_5; hence A is functional ; ::_thesis: verum end; end; definition let V, C be set ; let A, B be Element of Fin (PFuncs (V,C)); funcA ^ B -> Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3 { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; coherence { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C)) proof deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = \$1 \/ \$2; set M = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; set N = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ; A1: { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ) assume a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; ::_thesis: a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } then ex s, t being Element of PFuncs (V,C) st ( a = s \/ t & s in A & t in B & s tolerates t ) ; hence a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ; ::_thesis: verum end; A2: { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= PFuncs (V,C) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or y in PFuncs (V,C) ) assume y in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; ::_thesis: y in PFuncs (V,C) then consider s, t being Element of PFuncs (V,C) such that A3: y = s \/ t and s in A and t in B and A4: s tolerates t ; reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47; reconsider s9 = s, t9 = t as Function ; ( s is PartFunc of V,C & t is PartFunc of V,C ) by PARTFUN1:47; then s9 +* t9 is PartFunc of V,C by FUNCT_4:40; then s99 \/ t99 is PartFunc of V,C by A4, FUNCT_4:30; hence y in PFuncs (V,C) by A3, PARTFUN1:45; ::_thesis: verum end; A5: B is finite ; A6: A is finite ; { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } is finite from FRAENKEL:sch_22(A6, A5); hence { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def_5; ::_thesis: verum end; end; :: deftheorem defines ^ SUBSTLAT:def_3_:_ for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; theorem Th3: :: SUBSTLAT:3 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: A ^ B = B ^ A deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = \$1 \/ \$2; defpred S1[ Function, Function] means ( \$1 in A & \$2 in B & \$1 tolerates \$2 ); defpred S2[ Function, Function] means ( \$2 in B & \$1 in A & \$2 tolerates \$1 ); set X1 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } ; set X2 = { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } ; A1: now__::_thesis:_for_x_being_set_holds_ (_x_in__{__H1(t,s)_where_s,_t_is_Element_of_PFuncs_(V,C)_:_S2[s,t]__}__iff_x_in__{__(t_\/_s)_where_t,_s_is_Element_of_PFuncs_(V,C)_:_(_t_in_B_&_s_in_A_&_t_tolerates_s_)__}__) let x be set ; ::_thesis: ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff x in { (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s ) } ) ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff ex s, t being Element of PFuncs (V,C) st ( x = H1(t,s) & S2[s,t] ) ) ; then ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff ex t, s being Element of PFuncs (V,C) st ( x = t \/ s & t in B & s in A & t tolerates s ) ) ; hence ( x in { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } iff x in { (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s ) } ) ; ::_thesis: verum end; A2: for s, t being Element of PFuncs (V,C) holds H1(s,t) = H1(t,s) ; A3: for s, t being Element of PFuncs (V,C) holds ( S1[s,t] iff S2[s,t] ) ; { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } = { H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t] } from FRAENKEL:sch_8(A3, A2); hence A ^ B = B ^ A by A1, TARSKI:1; ::_thesis: verum end; theorem Th4: :: SUBSTLAT:4 for V, C being set for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds A ^ B = A proof let V, C be set ; ::_thesis: for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds A ^ B = A let B, A be Element of Fin (PFuncs (V,C)); ::_thesis: ( B = {{}} implies A ^ B = A ) A1: { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } c= A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } or a in A ) assume a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } ; ::_thesis: a in A then consider s9, t9 being Element of PFuncs (V,C) such that A2: ( a = s9 \/ t9 & s9 in A ) and A3: t9 in {{}} and s9 tolerates t9 ; t9 = {} by A3, TARSKI:def_1; hence a in A by A2; ::_thesis: verum end; A4: A c= { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } proof {} is PartFunc of V,C by RELSET_1:12; then reconsider b = {} as Element of PFuncs (V,C) by PARTFUN1:45; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } ) assume A5: a in A ; ::_thesis: a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } A c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider a9 = a as Element of PFuncs (V,C) by A5; A6: b in {{}} by TARSKI:def_1; ( a = a9 \/ b & a9 tolerates b ) by PARTFUN1:59; hence a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } by A5, A6; ::_thesis: verum end; assume B = {{}} ; ::_thesis: A ^ B = A hence A ^ B = A by A1, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th5: :: SUBSTLAT:5 for V, C being set for B being Element of Fin (PFuncs (V,C)) for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds a = b proof let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds a = b let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds a = b let a, b be set ; ::_thesis: ( B in SubstitutionSet (V,C) & a in B & b in B & a c= b implies a = b ) assume B in SubstitutionSet (V,C) ; ::_thesis: ( not a in B or not b in B or not a c= b or a = b ) then A1: ex A1 being Element of Fin (PFuncs (V,C)) st ( A1 = B & ( for u being set st u in A1 holds u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds s = t ) ) ; assume that A2: ( a in B & b in B ) and A3: a c= b ; ::_thesis: a = b B c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider a9 = a, b9 = b as Element of PFuncs (V,C) by A2; a9 = b9 by A1, A2, A3; hence a = b ; ::_thesis: verum end; theorem Th6: :: SUBSTLAT:6 for V, C being set for B being Element of Fin (PFuncs (V,C)) for a being set st a in mi B holds ( a in B & ( for b being set st b in B & b c= a holds b = a ) ) proof let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) for a being set st a in mi B holds ( a in B & ( for b being set st b in B & b c= a holds b = a ) ) let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in mi B holds ( a in B & ( for b being set st b in B & b c= a holds b = a ) ) let a be set ; ::_thesis: ( a in mi B implies ( a in B & ( for b being set st b in B & b c= a holds b = a ) ) ) assume a in mi B ; ::_thesis: ( a in B & ( for b being set st b in B & b c= a holds b = a ) ) then A1: ex t being Element of PFuncs (V,C) st ( a = t & t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in B & s c= t ) iff s = t ) ) ) ; hence a in B ; ::_thesis: for b being set st b in B & b c= a holds b = a let b be set ; ::_thesis: ( b in B & b c= a implies b = a ) assume that A2: b in B and A3: b c= a ; ::_thesis: b = a B c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider b9 = b as Element of PFuncs (V,C) by A2; b9 = a by A1, A2, A3; hence b = a ; ::_thesis: verum end; Lm2: for V, C being set for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds a in B ) holds A c= B proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds a in B ) holds A c= B let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: ( ( for a being set st a in A holds a in B ) implies A c= B ) assume A1: for a being set st a in A holds a in B ; ::_thesis: A c= B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ) assume x in A ; ::_thesis: x in B hence x in B by A1; ::_thesis: verum end; registration let V, C be set ; clusterV1() Function-like finite for Element of PFuncs (V,C); existence ex b1 being Element of PFuncs (V,C) st b1 is finite proof {} is PartFunc of V,C by RELSET_1:12; then reconsider e = {} as Element of PFuncs (V,C) by PARTFUN1:45; take e ; ::_thesis: e is finite thus e is finite ; ::_thesis: verum end; end; theorem Th7: :: SUBSTLAT:7 for V, C being set for B being Element of Fin (PFuncs (V,C)) for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds b = a ) holds a in mi B proof let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds b = a ) holds a in mi B let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds b = a ) holds a in mi B let a be finite set ; ::_thesis: ( a in B & ( for b being finite set st b in B & b c= a holds b = a ) implies a in mi B ) assume that A1: a in B and A2: for s being finite set st s in B & s c= a holds s = a ; ::_thesis: a in mi B B c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider a9 = a as Element of PFuncs (V,C) by A1; for s being Element of PFuncs (V,C) holds ( ( s in B & s c= a ) iff s = a ) by A1, A2; then a9 in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds ( ( s in B & s c= t ) iff s = t ) ) ) } ; hence a in mi B ; ::_thesis: verum end; theorem Th8: :: SUBSTLAT:8 for V, C being set for A being Element of Fin (PFuncs (V,C)) holds mi A c= A proof let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi A c= A let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi A c= A for a being set st a in mi A holds a in A by Th6; hence mi A c= A by TARSKI:def_3; ::_thesis: verum end; theorem :: SUBSTLAT:9 for V, C being set for A being Element of Fin (PFuncs (V,C)) st A = {} holds mi A = {} by Th8, XBOOLE_1:3; theorem Th10: :: SUBSTLAT:10 for V, C being set for B being Element of Fin (PFuncs (V,C)) for b being finite set st b in B holds ex c being set st ( c c= b & c in mi B ) proof let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) for b being finite set st b in B holds ex c being set st ( c c= b & c in mi B ) let B be Element of Fin (PFuncs (V,C)); ::_thesis: for b being finite set st b in B holds ex c being set st ( c c= b & c in mi B ) defpred S1[ set , set ] means \$1 c= \$2; let b be finite set ; ::_thesis: ( b in B implies ex c being set st ( c c= b & c in mi B ) ) assume A1: b in B ; ::_thesis: ex c being set st ( c c= b & c in mi B ) A2: B c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider b9 = b as Element of PFuncs (V,C) by A1; A3: for a, b, c being Element of PFuncs (V,C) st S1[a,b] & S1[b,c] holds S1[a,c] by XBOOLE_1:1; A4: for a being Element of PFuncs (V,C) holds S1[a,a] ; for a being Element of PFuncs (V,C) st a in B holds ex b being Element of PFuncs (V,C) st ( b in B & S1[b,a] & ( for c being Element of PFuncs (V,C) st c in B & S1[c,b] holds S1[b,c] ) ) from FRAENKEL:sch_23(A4, A3); then consider c being Element of PFuncs (V,C) such that A5: c in B and A6: c c= b9 and A7: for a being Element of PFuncs (V,C) st a in B & a c= c holds c c= a by A1; take c ; ::_thesis: ( c c= b & c in mi B ) thus c c= b by A6; ::_thesis: c in mi B now__::_thesis:_for_b_being_finite_set_st_b_in_B_&_b_c=_c_holds_ b_=_c let b be finite set ; ::_thesis: ( b in B & b c= c implies b = c ) assume that A8: b in B and A9: b c= c ; ::_thesis: b = c reconsider b9 = b as Element of PFuncs (V,C) by A2, A8; c c= b9 by A7, A8, A9; hence b = c by A9, XBOOLE_0:def_10; ::_thesis: verum end; hence c in mi B by A5, A6, Th7; ::_thesis: verum end; theorem Th11: :: SUBSTLAT:11 for V, C being set for K being Element of SubstitutionSet (V,C) holds mi K = K proof let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi K = K let K be Element of SubstitutionSet (V,C); ::_thesis: mi K = K thus mi K c= K by Th8; :: according to XBOOLE_0:def_10 ::_thesis: K c= mi K now__::_thesis:_for_a_being_set_st_a_in_K_holds_ a_in_mi_K let a be set ; ::_thesis: ( a in K implies a in mi K ) assume A1: a in K ; ::_thesis: a in mi K then ( a is finite & ( for b being finite set st b in K & b c= a holds b = a ) ) by Lm1, Th5; hence a in mi K by A1, Th7; ::_thesis: verum end; hence K c= mi K by Lm2; ::_thesis: verum end; theorem Th12: :: SUBSTLAT:12 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A \/ B) c= (mi A) \/ B now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_ a_in_(mi_A)_\/_B let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in (mi A) \/ B ) assume A1: a in mi (A \/ B) ; ::_thesis: a in (mi A) \/ B then reconsider a9 = a as finite set by Lm1; A2: a in A \/ B by A1, Th6; now__::_thesis:_a_in_(mi_A)_\/_B percases ( a in A or a in B ) by A2, XBOOLE_0:def_3; supposeA3: a in A ; ::_thesis: a in (mi A) \/ B now__::_thesis:_for_b_being_finite_set_st_b_in_A_&_b_c=_a_holds_ b_=_a let b be finite set ; ::_thesis: ( b in A & b c= a implies b = a ) assume b in A ; ::_thesis: ( b c= a implies b = a ) then b in A \/ B by XBOOLE_0:def_3; hence ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum end; then a9 in mi A by A3, Th7; hence a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum end; suppose a in B ; ::_thesis: a in (mi A) \/ B hence a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence a in (mi A) \/ B ; ::_thesis: verum end; hence mi (A \/ B) c= (mi A) \/ B by Lm2; ::_thesis: verum end; theorem Th13: :: SUBSTLAT:13 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) \/ B) = mi (A \/ B) A1: (mi A) \/ B c= A \/ B by Th8, XBOOLE_1:9; now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_\/_B)_holds_ a_in_mi_(A_\/_B) let a be set ; ::_thesis: ( a in mi ((mi A) \/ B) implies a in mi (A \/ B) ) assume A2: a in mi ((mi A) \/ B) ; ::_thesis: a in mi (A \/ B) then reconsider a9 = a as finite set by Lm1; A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_\/_B_&_b_c=_a_holds_ b_=_a let b be finite set ; ::_thesis: ( b in A \/ B & b c= a implies b = a ) assume that A4: b in A \/ B and A5: b c= a ; ::_thesis: b = a now__::_thesis:_b_=_a percases ( b in A or b in B ) by A4, XBOOLE_0:def_3; suppose b in A ; ::_thesis: b = a then consider c being set such that A6: c c= b and A7: c in mi A by Th10; ( c in (mi A) \/ B & c c= a ) by A5, A6, A7, XBOOLE_0:def_3, XBOOLE_1:1; then c = a by A2, Th6; hence b = a by A5, A6, XBOOLE_0:def_10; ::_thesis: verum end; suppose b in B ; ::_thesis: b = a then b in (mi A) \/ B by XBOOLE_0:def_3; hence b = a by A2, A5, Th6; ::_thesis: verum end; end; end; hence b = a ; ::_thesis: verum end; a in (mi A) \/ B by A2, Th6; then a9 in mi (A \/ B) by A1, A3, Th7; hence a in mi (A \/ B) ; ::_thesis: verum end; hence mi ((mi A) \/ B) c= mi (A \/ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A \/ B) c= mi ((mi A) \/ B) A8: mi (A \/ B) c= (mi A) \/ B by Th12; now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_ a_in_mi_((mi_A)_\/_B) let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in mi ((mi A) \/ B) ) assume A9: a in mi (A \/ B) ; ::_thesis: a in mi ((mi A) \/ B) then reconsider a9 = a as finite set by Lm1; for b being finite set st b in (mi A) \/ B & b c= a holds b = a by A1, A9, Th6; then a9 in mi ((mi A) \/ B) by A8, A9, Th7; hence a in mi ((mi A) \/ B) ; ::_thesis: verum end; hence mi (A \/ B) c= mi ((mi A) \/ B) by Lm2; ::_thesis: verum end; theorem Th14: :: SUBSTLAT:14 for V, C being set for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds A ^ D c= B ^ D proof let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds A ^ D c= B ^ D let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies A ^ D c= B ^ D ) deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = \$1 \/ \$2; defpred S1[ Function, Function] means ( \$1 in A & \$2 in D & \$1 tolerates \$2 ); defpred S2[ Function, Function] means ( \$1 in B & \$2 in D & \$1 tolerates \$2 ); set X1 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } ; set X2 = { H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t] } ; assume A c= B ; ::_thesis: A ^ D c= B ^ D then A1: for s, t being Element of PFuncs (V,C) st S1[s,t] holds S2[s,t] ; { H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t] } c= { H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t] } from FRAENKEL:sch_2(A1); hence A ^ D c= B ^ D ; ::_thesis: verum end; theorem Th15: :: SUBSTLAT:15 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) for a being set st a in A ^ B holds ex b, c being set st ( b in A & c in B & a = b \/ c ) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) for a being set st a in A ^ B holds ex b, c being set st ( b in A & c in B & a = b \/ c ) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds ex b, c being set st ( b in A & c in B & a = b \/ c ) let a be set ; ::_thesis: ( a in A ^ B implies ex b, c being set st ( b in A & c in B & a = b \/ c ) ) assume a in A ^ B ; ::_thesis: ex b, c being set st ( b in A & c in B & a = b \/ c ) then ex s, t being Element of PFuncs (V,C) st ( a = s \/ t & s in A & t in B & s tolerates t ) ; hence ex b, c being set st ( b in A & c in B & a = b \/ c ) ; ::_thesis: verum end; theorem :: SUBSTLAT:16 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds b \/ c in A ^ B ; Lm3: for V, C being set for A, B being Element of Fin (PFuncs (V,C)) for a being finite set st a in A ^ B holds ex b being finite set st ( b c= a & b in (mi A) ^ B ) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) for a being finite set st a in A ^ B holds ex b being finite set st ( b c= a & b in (mi A) ^ B ) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in A ^ B holds ex b being finite set st ( b c= a & b in (mi A) ^ B ) let a be finite set ; ::_thesis: ( a in A ^ B implies ex b being finite set st ( b c= a & b in (mi A) ^ B ) ) assume a in A ^ B ; ::_thesis: ex b being finite set st ( b c= a & b in (mi A) ^ B ) then consider b, c being Element of PFuncs (V,C) such that A1: a = b \/ c and A2: b in A and A3: c in B and A4: b tolerates c ; b is finite by A1, FINSET_1:1, XBOOLE_1:7; then consider d being set such that A5: d c= b and A6: d in mi A by A2, Th10; A7: mi A c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider d9 = d, c9 = c as Element of PFuncs (V,C) by A6; reconsider d1 = d, b1 = b, c1 = c as PartFunc of V,C by A6, A7, PARTFUN1:46; d1 c= b1 by A5; then A8: d9 tolerates c9 by A4, PARTFUN1:58; then d9 \/ c9 = d9 +* c9 by FUNCT_4:30; then reconsider e = d1 \/ c1 as Element of PFuncs (V,C) by PARTFUN1:45; reconsider e = e as finite set by A1, A5, FINSET_1:1, XBOOLE_1:9; take e ; ::_thesis: ( e c= a & e in (mi A) ^ B ) thus e c= a by A1, A5, XBOOLE_1:9; ::_thesis: e in (mi A) ^ B thus e in (mi A) ^ B by A3, A6, A8; ::_thesis: verum end; theorem Th17: :: SUBSTLAT:17 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ B) c= (mi A) ^ B A1: (mi A) ^ B c= A ^ B by Th8, Th14; now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_ a_in_(mi_A)_^_B let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in (mi A) ^ B ) assume A2: a in mi (A ^ B) ; ::_thesis: a in (mi A) ^ B then ( a in A ^ B & a is finite ) by Lm1, Th6; then ex b being finite set st ( b c= a & b in (mi A) ^ B ) by Lm3; hence a in (mi A) ^ B by A1, A2, Th6; ::_thesis: verum end; hence mi (A ^ B) c= (mi A) ^ B by Lm2; ::_thesis: verum end; theorem Th18: :: SUBSTLAT:18 for V, C being set for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds D ^ A c= D ^ B proof let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds D ^ A c= D ^ B let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies D ^ A c= D ^ B ) ( D ^ A = A ^ D & D ^ B = B ^ D ) by Th3; hence ( A c= B implies D ^ A c= D ^ B ) by Th14; ::_thesis: verum end; theorem Th19: :: SUBSTLAT:19 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) ^ B) = mi (A ^ B) A1: (mi A) ^ B c= A ^ B by Th8, Th14; now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_^_B)_holds_ a_in_mi_(A_^_B) let a be set ; ::_thesis: ( a in mi ((mi A) ^ B) implies a in mi (A ^ B) ) assume A2: a in mi ((mi A) ^ B) ; ::_thesis: a in mi (A ^ B) A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_^_B_&_b_c=_a_holds_ b_=_a let b be finite set ; ::_thesis: ( b in A ^ B & b c= a implies b = a ) assume b in A ^ B ; ::_thesis: ( b c= a implies b = a ) then consider c being finite set such that A4: c c= b and A5: c in (mi A) ^ B by Lm3; assume A6: b c= a ; ::_thesis: b = a then c c= a by A4, XBOOLE_1:1; then c = a by A2, A5, Th6; hence b = a by A4, A6, XBOOLE_0:def_10; ::_thesis: verum end; ( a in (mi A) ^ B & a is finite ) by A2, Lm1, Th6; hence a in mi (A ^ B) by A1, A3, Th7; ::_thesis: verum end; hence mi ((mi A) ^ B) c= mi (A ^ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A ^ B) c= mi ((mi A) ^ B) A7: mi (A ^ B) c= (mi A) ^ B by Th17; now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_ a_in_mi_((mi_A)_^_B) let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in mi ((mi A) ^ B) ) assume A8: a in mi (A ^ B) ; ::_thesis: a in mi ((mi A) ^ B) then ( a is finite & ( for b being finite set st b in (mi A) ^ B & b c= a holds b = a ) ) by A1, Lm1, Th6; hence a in mi ((mi A) ^ B) by A7, A8, Th7; ::_thesis: verum end; hence mi (A ^ B) c= mi ((mi A) ^ B) by Lm2; ::_thesis: verum end; theorem Th20: :: SUBSTLAT:20 for V, C being set for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ (mi B)) = mi (A ^ B) ( A ^ (mi B) = (mi B) ^ A & A ^ B = B ^ A ) by Th3; hence mi (A ^ (mi B)) = mi (A ^ B) by Th19; ::_thesis: verum end; theorem Th21: :: SUBSTLAT:21 for V, C being set for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M proof let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) = (K ^ L) ^ M A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th3; A2: now__::_thesis:_for_K,_L,_M_being_Element_of_Fin_(PFuncs_(V,C))_holds_K_^_(L_^_M)_c=_(K_^_L)_^_M let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) c= (K ^ L) ^ M A3: ( K c= PFuncs (V,C) & L c= PFuncs (V,C) ) by FINSUB_1:def_5; A4: M c= PFuncs (V,C) by FINSUB_1:def_5; now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_^_M)_holds_ a_in_(K_^_L)_^_M let a be set ; ::_thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M ) A5: K ^ (L ^ M) c= PFuncs (V,C) by FINSUB_1:def_5; assume A6: a in K ^ (L ^ M) ; ::_thesis: a in (K ^ L) ^ M then consider b, c being set such that A7: b in K and A8: c in L ^ M and A9: a = b \/ c by Th15; A10: c c= b \/ c by XBOOLE_1:7; consider b1, c1 being set such that A11: b1 in L and A12: c1 in M and A13: c = b1 \/ c1 by A8, Th15; reconsider b2 = b, b12 = b1 as PartFunc of V,C by A3, A7, A11, PARTFUN1:46; reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3, A4, A7, A11, A12; b1 c= c by A13, XBOOLE_1:7; then A14: ( b c= b \/ c & b1 c= b \/ c ) by A10, XBOOLE_1:1, XBOOLE_1:7; then A15: b9 tolerates b19 by A6, A9, A5, PARTFUN1:57; then b9 \/ b19 = b9 +* b19 by FUNCT_4:30; then b2 \/ b12 is PartFunc of V,C ; then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45; A16: ( b \/ (b1 \/ c1) = (b \/ b1) \/ c1 & c2 in K ^ L ) by A7, A11, A15, XBOOLE_1:4; c1 c= c by A13, XBOOLE_1:7; then A17: c1 c= b \/ c by A10, XBOOLE_1:1; c2 c= b \/ c by A14, XBOOLE_1:8; then c2 tolerates c19 by A6, A9, A5, A17, PARTFUN1:57; hence a in (K ^ L) ^ M by A9, A12, A13, A16; ::_thesis: verum end; hence K ^ (L ^ M) c= (K ^ L) ^ M by Lm2; ::_thesis: verum end; then A18: K ^ (L ^ M) c= (K ^ L) ^ M ; ( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th3; then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2; hence K ^ (L ^ M) = (K ^ L) ^ M by A18, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th22: :: SUBSTLAT:22 for V, C being set for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M) proof let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M) let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M) now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_\/_M)_holds_ a_in_(K_^_L)_\/_(K_^_M) let a be set ; ::_thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) ) assume A1: a in K ^ (L \/ M) ; ::_thesis: a in (K ^ L) \/ (K ^ M) then consider b, c being set such that A2: b in K and A3: c in L \/ M and A4: a = b \/ c by Th15; K ^ (L \/ M) c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider a9 = a as Element of PFuncs (V,C) by A1; ( K c= PFuncs (V,C) & L \/ M c= PFuncs (V,C) ) by FINSUB_1:def_5; then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2, A3; ( b9 c= a9 & c9 c= a9 ) by A4, XBOOLE_1:7; then A5: b9 tolerates c9 by PARTFUN1:57; ( c9 in L or c9 in M ) by A3, XBOOLE_0:def_3; then ( a in K ^ L or a in K ^ M ) by A2, A4, A5; hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def_3; ::_thesis: verum end; hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) ( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th18, XBOOLE_1:7; hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; ::_thesis: verum end; Lm4: for V, C being set for A, B being Element of Fin (PFuncs (V,C)) for a being set st a in A ^ B holds ex c being set st ( c in B & c c= a ) proof let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) for a being set st a in A ^ B holds ex c being set st ( c in B & c c= a ) let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds ex c being set st ( c in B & c c= a ) let a be set ; ::_thesis: ( a in A ^ B implies ex c being set st ( c in B & c c= a ) ) assume a in A ^ B ; ::_thesis: ex c being set st ( c in B & c c= a ) then consider b, c being set such that b in A and A1: c in B and A2: a = b \/ c by Th15; take c ; ::_thesis: ( c in B & c c= a ) thus c in B by A1; ::_thesis: c c= a thus c c= a by A2, XBOOLE_1:7; ::_thesis: verum end; Lm5: for V, C being set for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L proof let V, C be set ; ::_thesis: for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L let K, L be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((K ^ L) \/ L) = mi L now__::_thesis:_for_a_being_set_st_a_in_mi_((K_^_L)_\/_L)_holds_ a_in_mi_L let a be set ; ::_thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L ) assume A1: a in mi ((K ^ L) \/ L) ; ::_thesis: a in mi L then a in (K ^ L) \/ L by Th6; then A2: ( a in K ^ L or a in L ) by XBOOLE_0:def_3; A3: now__::_thesis:_for_b_being_finite_set_st_b_in_L_&_b_c=_a_holds_ b_=_a let b be finite set ; ::_thesis: ( b in L & b c= a implies b = a ) assume b in L ; ::_thesis: ( b c= a implies b = a ) then b in (K ^ L) \/ L by XBOOLE_0:def_3; hence ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum end; A4: now__::_thesis:_(_a_in_K_^_L_implies_a_in_L_) assume a in K ^ L ; ::_thesis: a in L then consider b being set such that A5: b in L and A6: b c= a by Lm4; b in (K ^ L) \/ L by A5, XBOOLE_0:def_3; hence a in L by A1, A5, A6, Th6; ::_thesis: verum end; a is finite by A1, Lm1; hence a in mi L by A2, A4, A3, Th7; ::_thesis: verum end; hence mi ((K ^ L) \/ L) c= mi L by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi L c= mi ((K ^ L) \/ L) now__::_thesis:_for_a_being_set_st_a_in_mi_L_holds_ a_in_mi_((K_^_L)_\/_L) let a be set ; ::_thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) ) assume A7: a in mi L ; ::_thesis: a in mi ((K ^ L) \/ L) then A8: a in L by Th6; then A9: a in (K ^ L) \/ L by XBOOLE_0:def_3; A10: now__::_thesis:_for_b_being_finite_set_st_b_in_(K_^_L)_\/_L_&_b_c=_a_holds_ b_=_a let b be finite set ; ::_thesis: ( b in (K ^ L) \/ L & b c= a implies b = a ) assume b in (K ^ L) \/ L ; ::_thesis: ( b c= a implies b = a ) then A11: ( b in K ^ L or b in L ) by XBOOLE_0:def_3; assume A12: b c= a ; ::_thesis: b = a now__::_thesis:_(_b_in_K_^_L_implies_b_in_L_) assume b in K ^ L ; ::_thesis: b in L then consider c being set such that A13: c in L and A14: c c= b by Lm4; c c= a by A12, A14, XBOOLE_1:1; then c = a by A7, A13, Th6; hence b in L by A8, A12, A14, XBOOLE_0:def_10; ::_thesis: verum end; hence b = a by A7, A11, A12, Th6; ::_thesis: verum end; a is finite by A7, Lm1; hence a in mi ((K ^ L) \/ L) by A9, A10, Th7; ::_thesis: verum end; hence mi L c= mi ((K ^ L) \/ L) by Lm2; ::_thesis: verum end; theorem Th23: :: SUBSTLAT:23 for V, C being set for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B proof let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B let B be Element of Fin (PFuncs (V,C)); ::_thesis: B c= B ^ B now__::_thesis:_for_a_being_set_st_a_in_B_holds_ a_in_B_^_B let a be set ; ::_thesis: ( a in B implies a in B ^ B ) assume A1: a in B ; ::_thesis: a in B ^ B B c= PFuncs (V,C) by FINSUB_1:def_5; then reconsider a9 = a as Element of PFuncs (V,C) by A1; ( a = a \/ a & a9 tolerates a9 ) ; hence a in B ^ B by A1; ::_thesis: verum end; hence B c= B ^ B by Lm2; ::_thesis: verum end; theorem Th24: :: SUBSTLAT:24 for V, C being set for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A proof let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ A) = mi A thus mi (A ^ A) = mi ((A ^ A) \/ A) by Th23, XBOOLE_1:12 .= mi A by Lm5 ; ::_thesis: verum end; theorem :: SUBSTLAT:25 for V, C being set for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K proof let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K let K be Element of SubstitutionSet (V,C); ::_thesis: mi (K ^ K) = K thus mi (K ^ K) = mi K by Th24 .= K by Th11 ; ::_thesis: verum end; begin definition let V, C be set ; func SubstLatt (V,C) -> strict LattStr means :Def4: :: SUBSTLAT:def 4 ( the carrier of it = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of it . (A,B) = mi (A \/ B) & the L_meet of it . (A,B) = mi (A ^ B) ) ) ); existence ex b1 being strict LattStr st ( the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) ) proof deffunc H1( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi (\$1 \/ \$2); consider j being BinOp of (SubstitutionSet (V,C)) such that A1: for x, y being Element of SubstitutionSet (V,C) holds j . (x,y) = H1(x,y) from BINOP_1:sch_4(); deffunc H2( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) -> Element of SubstitutionSet (V,C) = mi (\$1 ^ \$2); consider m being BinOp of (SubstitutionSet (V,C)) such that A2: for x, y being Element of SubstitutionSet (V,C) holds m . (x,y) = H2(x,y) from BINOP_1:sch_4(); take LattStr(# (SubstitutionSet (V,C)),j,m #) ; ::_thesis: ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) ) thus ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being strict LattStr st the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) & the carrier of b2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of b2 . (A,B) = mi (A \/ B) & the L_meet of b2 . (A,B) = mi (A ^ B) ) ) holds b1 = b2 proof let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) ) & the carrier of A2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ) implies A1 = A2 ) assume that A3: the carrier of A1 = SubstitutionSet (V,C) and A4: for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and A5: the carrier of A2 = SubstitutionSet (V,C) and A6: for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; ::_thesis: A1 = A2 reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (SubstitutionSet (V,C)) by A3, A5; now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a1_._(x,y)_=_a2_._(x,y) let x, y be Element of SubstitutionSet (V,C); ::_thesis: a1 . (x,y) = a2 . (x,y) thus a1 . (x,y) = mi (x \/ y) by A4 .= a2 . (x,y) by A6 ; ::_thesis: verum end; then A7: a1 = a2 by BINOP_1:2; now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a3_._(x,y)_=_a4_._(x,y) let x, y be Element of SubstitutionSet (V,C); ::_thesis: a3 . (x,y) = a4 . (x,y) thus a3 . (x,y) = mi (x ^ y) by A4 .= a4 . (x,y) by A6 ; ::_thesis: verum end; hence A1 = A2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines SubstLatt SUBSTLAT:def_4_:_ for V, C being set for b3 being strict LattStr holds ( b3 = SubstLatt (V,C) iff ( the carrier of b3 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds ( the L_join of b3 . (A,B) = mi (A \/ B) & the L_meet of b3 . (A,B) = mi (A ^ B) ) ) ) ); registration let V, C be set ; cluster SubstLatt (V,C) -> non empty strict ; coherence not SubstLatt (V,C) is empty proof the carrier of (SubstLatt (V,C)) = SubstitutionSet (V,C) by Def4; hence not SubstLatt (V,C) is empty ; ::_thesis: verum end; end; Lm6: for V, C being set for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a proof let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a set G = SubstLatt (V,C); let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "\/" b = b "\/" a reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4; a "\/" b = mi (b9 \/ a9) by Def4 .= b "\/" a by Def4 ; hence a "\/" b = b "\/" a ; ::_thesis: verum end; Lm7: for V, C being set for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4; set G = SubstLatt (V,C); a "\/" (b "\/" c) = the L_join of (SubstLatt (V,C)) . (a,(mi (b9 \/ c9))) by Def4 .= mi ((mi (b9 \/ c9)) \/ a9) by Def4 .= mi (a9 \/ (b9 \/ c9)) by Th13 .= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4 .= mi ((mi (a9 \/ b9)) \/ c9) by Th13 .= the L_join of (SubstLatt (V,C)) . ((mi (a9 \/ b9)),c9) by Def4 .= (a "\/" b) "\/" c by Def4 ; hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum end; Lm8: for V, C being set for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L proof let V, C be set ; ::_thesis: for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L let K, L be Element of SubstitutionSet (V,C); ::_thesis: the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L thus the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = the L_join of (SubstLatt (V,C)) . ((mi (K ^ L)),L) by Def4 .= mi ((mi (K ^ L)) \/ L) by Def4 .= mi ((K ^ L) \/ L) by Th13 .= mi L by Lm5 .= L by Th11 ; ::_thesis: verum end; Lm9: for V, C being set for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b proof let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b let a, b be Element of (SubstLatt (V,C)); ::_thesis: (a "/\" b) "\/" b = b reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4; set G = SubstLatt (V,C); thus (a "/\" b) "\/" b = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,b9)),b9) .= b by Lm8 ; ::_thesis: verum end; Lm10: for V, C being set for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a proof let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" b = b "/\" a reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4; a "/\" b = mi (a9 ^ b9) by Def4 .= mi (b9 ^ a9) by Th3 .= b "/\" a by Def4 ; hence a "/\" b = b "/\" a ; ::_thesis: verum end; Lm11: for V, C being set for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4; set G = SubstLatt (V,C); a "/\" (b "/\" c) = the L_meet of (SubstLatt (V,C)) . (a,(mi (b9 ^ c9))) by Def4 .= mi (a9 ^ (mi (b9 ^ c9))) by Def4 .= mi (a9 ^ (b9 ^ c9)) by Th20 .= mi ((a9 ^ b9) ^ c9) by Th21 .= mi ((mi (a9 ^ b9)) ^ c9) by Th19 .= the L_meet of (SubstLatt (V,C)) . ((mi (a9 ^ b9)),c9) by Def4 .= (a "/\" b) "/\" c by Def4 ; hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum end; Lm12: for V, C being set for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) proof let V, C be set ; ::_thesis: for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) let K, L, M be Element of SubstitutionSet (V,C); ::_thesis: the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) A1: the L_meet of (SubstLatt (V,C)) . (K,M) = mi (K ^ M) by Def4; ( the L_join of (SubstLatt (V,C)) . (L,M) = mi (L \/ M) & the L_meet of (SubstLatt (V,C)) . (K,L) = mi (K ^ L) ) by Def4; then reconsider La = the L_join of (SubstLatt (V,C)) . (L,M), Lb = the L_meet of (SubstLatt (V,C)) . (K,L), Lc = the L_meet of (SubstLatt (V,C)) . (K,M) as Element of SubstitutionSet (V,C) by A1; the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = mi (K ^ La) by Def4 .= mi (K ^ (mi (L \/ M))) by Def4 .= mi (K ^ (L \/ M)) by Th20 .= mi ((K ^ L) \/ (K ^ M)) by Th22 .= mi ((mi (K ^ L)) \/ (K ^ M)) by Th13 .= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th13 .= mi (Lb \/ (mi (K ^ M))) by Def4 .= mi (Lb \/ Lc) by Def4 ; hence the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) by Def4; ::_thesis: verum end; Lm13: for V, C being set for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a proof let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (a "\/" b) = a reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4; thus a "/\" (a "\/" b) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Lm12 .= the L_join of (SubstLatt (V,C)) . ((mi (a9 ^ a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Def4 .= the L_join of (SubstLatt (V,C)) . ((mi a9),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Th24 .= a "\/" (a "/\" b) by Th11 .= (a "/\" b) "\/" a by Lm6 .= (b "/\" a) "\/" a by Lm10 .= a by Lm9 ; ::_thesis: verum end; registration let V, C be set ; cluster SubstLatt (V,C) -> strict Lattice-like ; coherence SubstLatt (V,C) is Lattice-like proof set G = SubstLatt (V,C); thus for u, v being Element of (SubstLatt (V,C)) holds u "\/" v = v "\/" u by Lm6; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( SubstLatt (V,C) is join-associative & SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing ) thus for u, v, w being Element of (SubstLatt (V,C)) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm7; :: according to LATTICES:def_5 ::_thesis: ( SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing ) thus for u, v being Element of (SubstLatt (V,C)) holds (u "/\" v) "\/" v = v by Lm9; :: according to LATTICES:def_8 ::_thesis: ( SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing ) thus for u, v being Element of (SubstLatt (V,C)) holds u "/\" v = v "/\" u by Lm10; :: according to LATTICES:def_6 ::_thesis: ( SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing ) thus for u, v, w being Element of (SubstLatt (V,C)) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm11; :: according to LATTICES:def_7 ::_thesis: SubstLatt (V,C) is join-absorbing let u, v be Element of (SubstLatt (V,C)); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u thus u "/\" (u "\/" v) = u by Lm13; ::_thesis: verum end; end; registration let V, C be set ; cluster SubstLatt (V,C) -> strict distributive bounded ; coherence ( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded ) proof thus SubstLatt (V,C) is distributive ::_thesis: SubstLatt (V,C) is bounded proof let u, v, w be Element of (SubstLatt (V,C)); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w) reconsider K = u, L = v, M = w as Element of SubstitutionSet (V,C) by Def4; thus u "/\" (v "\/" w) = the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) .= (u "/\" v) "\/" (u "/\" w) by Lm12 ; ::_thesis: verum end; A1: SubstLatt (V,C) is lower-bounded proof reconsider E = {} as Element of SubstitutionSet (V,C) by Th1; set L = SubstLatt (V,C); reconsider e = E as Element of (SubstLatt (V,C)) by Def4; take e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds ( e "/\" b1 = e & b1 "/\" e = e ) let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "/\" u = e & u "/\" e = e ) reconsider K = u as Element of SubstitutionSet (V,C) by Def4; A2: e "\/" u = mi (E \/ K) by Def4 .= u by Th11 ; then u "/\" e = e by LATTICES:def_9; hence ( e "/\" u = e & u "/\" e = e ) by A2, LATTICES:def_9; ::_thesis: verum end; SubstLatt (V,C) is upper-bounded proof reconsider E = {{}} as Element of SubstitutionSet (V,C) by Th2; set L = SubstLatt (V,C); reconsider e = E as Element of (SubstLatt (V,C)) by Def4; take e ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds ( e "\/" b1 = e & b1 "\/" e = e ) let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "\/" u = e & u "\/" e = e ) reconsider K = u as Element of SubstitutionSet (V,C) by Def4; A3: e "/\" u = mi (E ^ K) by Def4 .= mi (K ^ E) by Th3 .= mi K by Th4 .= u by Th11 ; then e "\/" u = e by LATTICES:def_8; hence ( e "\/" u = e & u "\/" e = e ) by A3, LATTICES:def_8; ::_thesis: verum end; hence SubstLatt (V,C) is bounded by A1; ::_thesis: verum end; end; theorem :: SUBSTLAT:26 for V, C being set holds Bottom (SubstLatt (V,C)) = {} proof let V, C be set ; ::_thesis: Bottom (SubstLatt (V,C)) = {} {} in SubstitutionSet (V,C) by Th1; then reconsider Z = {} as Element of (SubstLatt (V,C)) by Def4; now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"\/"_u_=_u let u be Element of (SubstLatt (V,C)); ::_thesis: Z "\/" u = u reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4; thus Z "\/" u = mi (z \/ u9) by Def4 .= u by Th11 ; ::_thesis: verum end; hence Bottom (SubstLatt (V,C)) = {} by LATTICE2:14; ::_thesis: verum end; theorem :: SUBSTLAT:27 for V, C being set holds Top (SubstLatt (V,C)) = {{}} proof let V, C be set ; ::_thesis: Top (SubstLatt (V,C)) = {{}} {{}} in SubstitutionSet (V,C) by Th2; then reconsider Z = {{}} as Element of (SubstLatt (V,C)) by Def4; now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"/\"_u_=_u let u be Element of (SubstLatt (V,C)); ::_thesis: Z "/\" u = u reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4; thus Z "/\" u = mi (z ^ u9) by Def4 .= mi (u9 ^ z) by Th3 .= mi u9 by Th4 .= u by Th11 ; ::_thesis: verum end; hence Top (SubstLatt (V,C)) = {{}} by LATTICE2:16; ::_thesis: verum end;