:: MSUALG_7 semantic presentation

begin


theorem Th1: :: MSUALG_7:1
for I being non empty set
for M being ManySortedSet of I holds id M is Equivalence_Relation of M
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds id M is Equivalence_Relation of M
let M be ManySortedSet of I; ::_thesis: id M is Equivalence_Relation of M
set J = id M;
 for i being set st i in I holds
(id M) . i is Relation of (M . i)
proof
let i be set ; ::_thesis: ( i in I implies (id M) . i is Relation of (M . i) )
assume  i in I ; ::_thesis: (id M) . i is Relation of (M . i)
then  (id M) . i = id (M . i) by MSUALG_3:def_1;
hence  (id M) . i is Relation of (M . i) ; ::_thesis: verum
end;
then reconsider J = id M as ManySortedRelation of M by MSUALG_4:def_1;
 for i being set
for R being Relation of (M . i) st i in I & J . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & J . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & J . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A1: i in I and
A2: J . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
 J . i = id (M . i) by A1, MSUALG_3:def_1;
hence  R is Equivalence_Relation of (M . i) by A2, EQREL_1:3; ::_thesis: verum
end;
hence  id M is Equivalence_Relation of M by MSUALG_4:def_2; ::_thesis: verum
end;

theorem Th2: :: MSUALG_7:2
for I being non empty set
for M being ManySortedSet of I holds [|M,M|] is Equivalence_Relation of M
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds [|M,M|] is Equivalence_Relation of M
let M be ManySortedSet of I; ::_thesis: [|M,M|] is Equivalence_Relation of M
set J = [|M,M|];
 for i being set st i in I holds
[|M,M|] . i is Relation of (M . i)
proof
let i be set ; ::_thesis: ( i in I implies [|M,M|] . i is Relation of (M . i) )
assume  i in I ; ::_thesis: [|M,M|] . i is Relation of (M . i)
then  [|M,M|] . i c= [:(M . i),(M . i):] by PBOOLE:def_16;
hence  [|M,M|] . i is Relation of (M . i) ; ::_thesis: verum
end;
then reconsider J = [|M,M|] as ManySortedRelation of M by MSUALG_4:def_1;
 for i being set
for R being Relation of (M . i) st i in I & J . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & J . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & J . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A1: i in I and
A2: J . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
J . i = [:(M . i),(M . i):] by A1, PBOOLE:def_16
.= nabla (M . i) by EQREL_1:def_1 ;
hence  R is Equivalence_Relation of (M . i) by A2, EQREL_1:4; ::_thesis: verum
end;
hence  [|M,M|] is Equivalence_Relation of M by MSUALG_4:def_2; ::_thesis: verum
end;

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster EqRelLatt M ->  bounded ;
coherence
 EqRelLatt M is bounded
proof
 ex c being Element of (EqRelLatt M) st
for a being Element of (EqRelLatt M) holds
( c "\/" a = c & a "\/" c = c )
proof
reconsider c9 = [|M,M|] as Equivalence_Relation of M by Th2;
reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def_5;
take  c ; ::_thesis: for a being Element of (EqRelLatt M) holds
( c "\/" a = c & a "\/" c = c )
let a be Element of (EqRelLatt M); ::_thesis: ( c "\/" a = c & a "\/" c = c )
reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def_5;
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(c9_"\/"_a9)_._i_=_c9_._i
let i be set ; ::_thesis: ( i in I implies (c9 "\/" a9) . i = c9 . i )
A2: ex K1 being ManySortedRelation of M st
( K1 = c9 \/ a9 & c9 "\/" a9 = EqCl K1 ) by MSUALG_5:def_4;
assume A3: i in I ; ::_thesis: (c9 "\/" a9) . i = c9 . i
then reconsider i9 = i as Element of I ;
reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
(c9 \/ a9) . i = (c9 . i) \/ (a9 . i) by A3, PBOOLE:def_4
.= [:(M . i),(M . i):] \/ (a9 . i) by A3, PBOOLE:def_16
.= (nabla (M . i)) \/ a2 by EQREL_1:def_1
.= nabla (M . i) by EQREL_1:1
.= [:(M . i),(M . i):] by EQREL_1:def_1
.= c9 . i by A3, PBOOLE:def_16 ;
hence (c9 "\/" a9) . i = EqCl K2 by A2, MSUALG_5:def_3
.= c9 . i by MSUALG_5:2 ;
::_thesis: verum
end;
thus c "\/" a = the L_join of (EqRelLatt M) . (c,a) by LATTICES:def_1
.= c9 "\/" a9 by MSUALG_5:def_5
.= c by A1, PBOOLE:3 ; ::_thesis: a "\/" c = c
hence  a "\/" c = c ; ::_thesis: verum
end;
then A4: EqRelLatt M is upper-bounded by LATTICES:def_14;
 ex c being Element of (EqRelLatt M) st
for a being Element of (EqRelLatt M) holds
( c "/\" a = c & a "/\" c = c )
proof
reconsider c9 = id M as Equivalence_Relation of M by Th1;
reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def_5;
take  c ; ::_thesis: for a being Element of (EqRelLatt M) holds
( c "/\" a = c & a "/\" c = c )
let a be Element of (EqRelLatt M); ::_thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def_5;
A5: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(c9_/\_a9)_._i_=_c9_._i
let i be set ; ::_thesis: ( i in I implies (c9 /\ a9) . i = c9 . i )
assume A6: i in I ; ::_thesis: (c9 /\ a9) . i = c9 . i
then reconsider i9 = i as Element of I ;
reconsider a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
thus (c9 /\ a9) . i = (c9 . i) /\ (a9 . i) by A6, PBOOLE:def_5
.= (id (M . i)) /\ a2 by MSUALG_3:def_1
.= id (M . i) by EQREL_1:10
.= c9 . i by A6, MSUALG_3:def_1 ; ::_thesis: verum
end;
thus c "/\" a = the L_meet of (EqRelLatt M) . (c,a) by LATTICES:def_2
.= c9 /\ a9 by MSUALG_5:def_5
.= c by A5, PBOOLE:3 ; ::_thesis: a "/\" c = c
hence  a "/\" c = c ; ::_thesis: verum
end;
then  EqRelLatt M is lower-bounded by LATTICES:def_13;
hence  EqRelLatt M is bounded by A4; ::_thesis: verum
end;
end;

theorem :: MSUALG_7:3
for I being non empty set
for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M
let M be ManySortedSet of I; ::_thesis: Bottom (EqRelLatt M) = id M
set K = id M;
 id M is Equivalence_Relation of M by Th1;
then reconsider K = id M as Element of (EqRelLatt M) by MSUALG_5:def_5;
now__::_thesis:_for_a_being_Element_of_(EqRelLatt_M)_holds_
(_K_"/\"_a_=_K_&_a_"/\"_K_=_K_)
let a be Element of (EqRelLatt M); ::_thesis: ( K "/\" a = K & a "/\" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def_5;
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(K9_/\_a9)_._i_=_K9_._i
let i be set ; ::_thesis: ( i in I implies (K9 /\ a9) . i = K9 . i )
assume A2: i in I ; ::_thesis: (K9 /\ a9) . i = K9 . i
then reconsider i9 = i as Element of I ;
reconsider a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
thus (K9 /\ a9) . i = (K9 . i) /\ (a9 . i) by A2, PBOOLE:def_5
.= (id (M . i)) /\ a2 by MSUALG_3:def_1
.= id (M . i) by EQREL_1:10
.= K9 . i by A2, MSUALG_3:def_1 ; ::_thesis: verum
end;
thus K "/\" a = the L_meet of (EqRelLatt M) . (K,a) by LATTICES:def_2
.= K9 /\ a9 by MSUALG_5:def_5
.= K by A1, PBOOLE:3 ; ::_thesis: a "/\" K = K
hence  a "/\" K = K ; ::_thesis: verum
end;
hence  Bottom (EqRelLatt M) = id M by LATTICES:def_16; ::_thesis: verum
end;

theorem :: MSUALG_7:4
for I being non empty set
for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]
let M be ManySortedSet of I; ::_thesis: Top (EqRelLatt M) = [|M,M|]
set K = [|M,M|];
 [|M,M|] is Equivalence_Relation of M by Th2;
then reconsider K = [|M,M|] as Element of (EqRelLatt M) by MSUALG_5:def_5;
now__::_thesis:_for_a_being_Element_of_(EqRelLatt_M)_holds_
(_K_"\/"_a_=_K_&_a_"\/"_K_=_K_)
let a be Element of (EqRelLatt M); ::_thesis: ( K "\/" a = K & a "\/" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def_5;
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(K9_"\/"_a9)_._i_=_K9_._i
let i be set ; ::_thesis: ( i in I implies (K9 "\/" a9) . i = K9 . i )
A2: ex K1 being ManySortedRelation of M st
( K1 = K9 \/ a9 & K9 "\/" a9 = EqCl K1 ) by MSUALG_5:def_4;
assume A3: i in I ; ::_thesis: (K9 "\/" a9) . i = K9 . i
then reconsider i9 = i as Element of I ;
reconsider K2 = K9 . i9, a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
(K9 \/ a9) . i = (K9 . i) \/ (a9 . i) by A3, PBOOLE:def_4
.= [:(M . i),(M . i):] \/ (a9 . i) by A3, PBOOLE:def_16
.= (nabla (M . i)) \/ a2 by EQREL_1:def_1
.= nabla (M . i) by EQREL_1:1
.= [:(M . i),(M . i):] by EQREL_1:def_1
.= K9 . i by A3, PBOOLE:def_16 ;
hence (K9 "\/" a9) . i = EqCl K2 by A2, MSUALG_5:def_3
.= K9 . i by MSUALG_5:2 ;
::_thesis: verum
end;
thus K "\/" a = the L_join of (EqRelLatt M) . (K,a) by LATTICES:def_1
.= K9 "\/" a9 by MSUALG_5:def_5
.= K by A1, PBOOLE:3 ; ::_thesis: a "\/" K = K
hence  a "\/" K = K ; ::_thesis: verum
end;
hence  Top (EqRelLatt M) = [|M,M|] by LATTICES:def_17; ::_thesis: verum
end;

theorem Th5: :: MSUALG_7:5
for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]
let M be ManySortedSet of I; ::_thesis: for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]
let X be Subset of (EqRelLatt M); ::_thesis: X is SubsetFamily of [|M,M|]
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(EqRelLatt_M)_holds_
x_in_Bool_[|M,M|]
let x be set ; ::_thesis: ( x in the carrier of (EqRelLatt M) implies x in Bool [|M,M|] )
assume  x in the carrier of (EqRelLatt M) ; ::_thesis: x in Bool [|M,M|]
then reconsider x9 = x as Equivalence_Relation of M by MSUALG_5:def_5;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
x9_._i_c=_[|M,M|]_._i
let i be set ; ::_thesis: ( i in I implies x9 . i c= [|M,M|] . i )
assume  i in I ; ::_thesis: x9 . i c= [|M,M|] . i
then reconsider i9 = i as Element of I ;
 x9 . i9 c= [:(M . i9),(M . i9):] ;
hence  x9 . i c= [|M,M|] . i by PBOOLE:def_16; ::_thesis: verum
end;
then  x9 c= [|M,M|] by PBOOLE:def_2;
then  x9 is ManySortedSubset of [|M,M|] by PBOOLE:def_18;
hence  x in Bool [|M,M|] by CLOSURE2:def_1; ::_thesis: verum
end;
then  the carrier of (EqRelLatt M) c= Bool [|M,M|] by TARSKI:def_3;
then  bool the carrier of (EqRelLatt M) c= bool (Bool [|M,M|]) by ZFMISC_1:67;
hence  X is SubsetFamily of [|M,M|] by TARSKI:def_3; ::_thesis: verum
end;

theorem Th6: :: MSUALG_7:6
for I being non empty set
for M being ManySortedSet of I
for a, b being Element of (EqRelLatt M)
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for a, b being Element of (EqRelLatt M)
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )
let M be ManySortedSet of I; ::_thesis: for a, b being Element of (EqRelLatt M)
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )
let a, b be Element of (EqRelLatt M); ::_thesis: for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )
let A, B be Equivalence_Relation of M; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a [= b iff A c= B )
thus  ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b )
proof
assume A3: a [= b ; ::_thesis: A c= B
A /\ B = the L_meet of (EqRelLatt M) . (A,B) by MSUALG_5:def_5
.= a "/\" b by A1, A2, LATTICES:def_2
.= A by A1, A3, LATTICES:4 ;
hence  A c= B by PBOOLE:15; ::_thesis: verum
end;
thus  ( A c= B implies a [= b ) ::_thesis: verum
proof
assume A4: A c= B ; ::_thesis: a [= b
a "/\" b = the L_meet of (EqRelLatt M) . (A,B) by A1, A2, LATTICES:def_2
.= A /\ B by MSUALG_5:def_5
.= a by A1, A4, PBOOLE:23 ;
hence  a [= b by LATTICES:4; ::_thesis: verum
end;
end;

theorem Th7: :: MSUALG_7:7
for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let M be ManySortedSet of I; ::_thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let X be Subset of (EqRelLatt M); ::_thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let X1 be SubsetFamily of [|M,M|]; ::_thesis: ( X1 = X implies for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b )
assume A1: X1 = X ; ::_thesis: for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let a, b be Equivalence_Relation of M; ::_thesis: ( a = meet |:X1:| & b in X implies a c= b )
assume that
A2: a = meet |:X1:| and
A3: b in X ; ::_thesis: a c= b
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
a_._i_c=_b_._i
reconsider b9 = b as Element of Bool [|M,M|] by A1, A3;
let i be set ; ::_thesis: ( i in I implies a . i c= b . i )
assume A4: i in I ; ::_thesis: a . i c= b . i
then  |:X1:| . i =  {  (x . i) where x is Element of Bool [|M,M|] : x in X1  }  by A1, A3, CLOSURE2:14;
then A5: b9 . i in |:X1:| . i by A1, A3;
then A6: for y being set st y in meet (|:X1:| . i) holds
y in b . i by SETFAM_1:def_1;
 ex Q being Subset-Family of ([|M,M|] . i) st
( Q = |:X1:| . i & (meet |:X1:|) . i = Intersect Q ) by A4, MSSUBFAM:def_1;
then  a . i = meet (|:X1:| . i) by A2, A5, SETFAM_1:def_9;
hence  a . i c= b . i by A6, TARSKI:def_3; ::_thesis: verum
end;
hence  a c= b by PBOOLE:def_2; ::_thesis: verum
end;

theorem Th8: :: MSUALG_7:8
for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let M be ManySortedSet of I; ::_thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X be Subset of (EqRelLatt M); ::_thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X1 be SubsetFamily of [|M,M|]; ::_thesis: ( X1 = X & not X is empty implies meet |:X1:| is Equivalence_Relation of M )
set a = meet |:X1:|;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(meet_|:X1:|)_._i_is_Relation_of_(M_._i)
let i be set ; ::_thesis: ( i in I implies (meet |:X1:|) . i is Relation of (M . i) )
assume A1: i in I ; ::_thesis: (meet |:X1:|) . i is Relation of (M . i)
 meet |:X1:| c= [|M,M|] by PBOOLE:def_18;
then  (meet |:X1:|) . i c= [|M,M|] . i by A1, PBOOLE:def_2;
hence  (meet |:X1:|) . i is Relation of (M . i) by A1, PBOOLE:def_16; ::_thesis: verum
end;
then reconsider a = meet |:X1:| as ManySortedRelation of M by MSUALG_4:def_1;
assume that
A2: X1 = X and
A3: not X is empty ; ::_thesis: meet |:X1:| is Equivalence_Relation of M
now__::_thesis:_for_i_being_set_
for_R_being_Relation_of_(M_._i)_st_i_in_I_&_a_._i_=_R_holds_
R_is_Equivalence_Relation_of_(M_._i)
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2, A3;
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & a . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & a . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A4: i in I and
A5: a . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A4;
reconsider b = |:X1:| . i9 as Subset-Family of [:(M . i),(M . i):] by PBOOLE:def_16;
consider Q being Subset-Family of ([|M,M|] . i) such that
A6: Q = |:X1:| . i and
A7: R = Intersect Q by A4, A5, MSSUBFAM:def_1;
reconsider Q = Q as Subset-Family of [:(M . i),(M . i):] by A4, PBOOLE:def_16;
 |:X19:| is V2() ;
then A8: Q <> {} by A4, A6, PBOOLE:def_13;
A9: |:X19:| . i =  {  (x . i) where x is Element of Bool [|M,M|] : x in X1  }  by A4, CLOSURE2:14;
now__::_thesis:_for_Y_being_set_st_Y_in_b_holds_
Y_is_Equivalence_Relation_of_(M_._i)
let Y be set ; ::_thesis: ( Y in b implies Y is Equivalence_Relation of (M . i) )
assume  Y in b ; ::_thesis: Y is Equivalence_Relation of (M . i)
then consider z being Element of Bool [|M,M|] such that
A10: Y = z . i and
A11: z in X by A2, A9;
 z c= [|M,M|] by PBOOLE:def_18;
then  z . i c= [|M,M|] . i by A4, PBOOLE:def_2;
then reconsider Y1 = Y as Relation of (M . i) by A4, A10, PBOOLE:def_16;
 z is Equivalence_Relation of M by A11, MSUALG_5:def_5;
then  Y1 is Equivalence_Relation of (M . i) by A4, A10, MSUALG_4:def_2;
hence  Y is Equivalence_Relation of (M . i) ; ::_thesis: verum
end;
then  meet b is Equivalence_Relation of (M . i) by A6, A8, EQREL_1:11;
hence  R is Equivalence_Relation of (M . i) by A6, A7, A8, SETFAM_1:def_9; ::_thesis: verum
end;
hence  meet |:X1:| is Equivalence_Relation of M by MSUALG_4:def_2; ::_thesis: verum
end;

definition
let L be non empty LattStr ;
redefine attr L is complete  means :Def1: :: MSUALG_7:def 1
 for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) );
compatibility
 ( L is complete iff for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) )
proof
thus  ( L is complete implies for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ) by LATTICE3:def_18; ::_thesis: ( ( for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ) implies L is complete )
assume A1: for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) ; ::_thesis: L is complete
let X be set ; :: according to LATTICE3:def_18 ::_thesis: ex b1 being Element of the carrier of L st
( X is_less_than b1 & ( for b2 being Element of the carrier of L holds
( not X is_less_than b2 or b1 [= b2 ) ) )
defpred S1[ set ] means $1 in X;
set Y =  {  c where c is Element of L : S1[c]  }  ;
  {  c where c is Element of L : S1[c]  }  is Subset of L from DOMAIN_1:sch_7();
then consider p being Element of L such that
A2:  {  c where c is Element of L : S1[c]  }  is_less_than p and
A3: for r being Element of L st  {  c where c is Element of L : S1[c]  }  is_less_than r holds
p [= r by A1;
take  p ; ::_thesis: ( X is_less_than p & ( for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 ) ) )
thus  X is_less_than p ::_thesis: for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 )
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X or q [= p )
assume  q in X ; ::_thesis: q [= p
then  q in  {  c where c is Element of L : S1[c]  }  ;
hence  q [= p by A2, LATTICE3:def_17; ::_thesis: verum
end;
let r be Element of L; ::_thesis: ( not X is_less_than r or p [= r )
assume A4: X is_less_than r ; ::_thesis: p [= r
now__::_thesis:_for_q_being_Element_of_L_st_q_in__{__c_where_c_is_Element_of_L_:_S1[c]__}__holds_
q_[=_r
let q be Element of L; ::_thesis: ( q in  {  c where c is Element of L : S1[c]  }  implies q [= r )
assume  q in  {  c where c is Element of L : S1[c]  }  ; ::_thesis: q [= r
then  ex v being Element of L st
( q = v & v in X ) ;
hence  q [= r by A4, LATTICE3:def_17; ::_thesis: verum
end;
then   {  c where c is Element of L : S1[c]  }  is_less_than r by LATTICE3:def_17;
hence  p [= r by A3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines complete MSUALG_7:def_1_:_
 for L being non empty LattStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( X is_less_than a & ( for b being Element of L st X is_less_than b holds
a [= b ) ) );

theorem Th9: :: MSUALG_7:9
for I being non empty set
for M being ManySortedSet of I holds EqRelLatt M is complete
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds EqRelLatt M is complete
let M be ManySortedSet of I; ::_thesis: EqRelLatt M is complete
 for X being Subset of (EqRelLatt M) ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
proof
let X be Subset of (EqRelLatt M); ::_thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
reconsider X1 = X as SubsetFamily of [|M,M|] by Th5;
percases ( X is empty or not X is empty ) ;
supposeA1: X is empty ; ::_thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
take a = Top (EqRelLatt M); ::_thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
 for q being Element of (EqRelLatt M) st q in X holds
a [= q by A1;
hence  a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a
let b be Element of (EqRelLatt M); ::_thesis: ( b is_less_than X implies b [= a )
assume  b is_less_than X ; ::_thesis: b [= a
thus  b [= a by LATTICES:19; ::_thesis: verum
end;
supposeA2: not X is empty ; ::_thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
then reconsider a = meet |:X1:| as Equivalence_Relation of M by Th8;
set a9 = a;
reconsider a = a as Element of (EqRelLatt M) by MSUALG_5:def_5;
take  a ; ::_thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
now__::_thesis:_for_q_being_Element_of_(EqRelLatt_M)_st_q_in_X_holds_
a_[=_q
let q be Element of (EqRelLatt M); ::_thesis: ( q in X implies a [= q )
reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def_5;
assume  q in X ; ::_thesis: a [= q
then  a c= q9 by Th7;
hence  a [= q by Th6; ::_thesis: verum
end;
hence  a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a
now__::_thesis:_for_b_being_Element_of_(EqRelLatt_M)_st_b_is_less_than_X_holds_
b_[=_a
let b be Element of (EqRelLatt M); ::_thesis: ( b is_less_than X implies b [= a )
reconsider b9 = b as Equivalence_Relation of M by MSUALG_5:def_5;
assume A3: b is_less_than X ; ::_thesis: b [= a
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
b9_._i_c=_(meet_|:X1:|)_._i
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2;
let i be set ; ::_thesis: ( i in I implies b9 . i c= (meet |:X1:|) . i )
assume A4: i in I ; ::_thesis: b9 . i c= (meet |:X1:|) . i
then A5: ex Q being Subset-Family of ([|M,M|] . i) st
( Q = |:X1:| . i & (meet |:X1:|) . i = Intersect Q ) by MSSUBFAM:def_1;
 |:X19:| is V2() ;
then A6: |:X1:| . i <> {} by A4, PBOOLE:def_13;
now__::_thesis:_for_Z_being_set_st_Z_in_|:X1:|_._i_holds_
b9_._i_c=_Z
let Z be set ; ::_thesis: ( Z in |:X1:| . i implies b9 . i c= Z )
assume A7: Z in |:X1:| . i ; ::_thesis: b9 . i c= Z
 |:X19:| . i =  {  (x . i) where x is Element of Bool [|M,M|] : x in X1  }  by A4, CLOSURE2:14;
then consider z being Element of Bool [|M,M|] such that
A8: Z = z . i and
A9: z in X1 by A7;
reconsider z9 = z as Element of (EqRelLatt M) by A9;
reconsider z99 = z9 as Equivalence_Relation of M by MSUALG_5:def_5;
 b [= z9 by A3, A9, LATTICE3:def_16;
then  b9 c= z99 by Th6;
hence  b9 . i c= Z by A4, A8, PBOOLE:def_2; ::_thesis: verum
end;
then  b9 . i c= meet (|:X1:| . i) by A6, SETFAM_1:5;
hence  b9 . i c= (meet |:X1:|) . i by A6, A5, SETFAM_1:def_9; ::_thesis: verum
end;
then  b9 c= meet |:X1:| by PBOOLE:def_2;
hence  b [= a by Th6; ::_thesis: verum
end;
hence  for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ; ::_thesis: verum
end;
end;
end;
hence  EqRelLatt M is complete by VECTSP_8:def_6; ::_thesis: verum
end;

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster EqRelLatt M ->  complete ;
coherence
 EqRelLatt M is complete by Th9;
end;

theorem :: MSUALG_7:10
for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b
let M be ManySortedSet of I; ::_thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b
let X be Subset of (EqRelLatt M); ::_thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b
let X1 be SubsetFamily of [|M,M|]; ::_thesis: ( X1 = X & not X is empty implies for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b )
assume that
A1: X1 = X and
A2: not X is empty ; ::_thesis: for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) holds
a = b
let a, b be Equivalence_Relation of M; ::_thesis: ( a = meet |:X1:| & b = "/\" (X,(EqRelLatt M)) implies a = b )
reconsider a9 = a as Element of (EqRelLatt M) by MSUALG_5:def_5;
assume that
A3: a = meet |:X1:| and
A4: b = "/\" (X,(EqRelLatt M)) ; ::_thesis: a = b
A5: now__::_thesis:_for_c_being_Element_of_(EqRelLatt_M)_st_c_is_less_than_X_holds_
c_[=_a9
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A1, A2;
let c be Element of (EqRelLatt M); ::_thesis: ( c is_less_than X implies c [= a9 )
reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def_5;
reconsider S = |:X19:| as V2() MSSubsetFamily of [|M,M|] ;
assume A6: c is_less_than X ; ::_thesis: c [= a9
now__::_thesis:_for_Z1_being_ManySortedSet_of_I_st_Z1_in_S_holds_
c9_c=_Z1
let Z1 be ManySortedSet of I; ::_thesis: ( Z1 in S implies c9 c= Z1 )
assume A7: Z1 in S ; ::_thesis: c9 c= Z1
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
c9_._i_c=_Z1_._i
let i be set ; ::_thesis: ( i in I implies c9 . i c= Z1 . i )
assume A8: i in I ; ::_thesis: c9 . i c= Z1 . i
then  ( Z1 . i in |:X1:| . i & |:X19:| . i =  {  (x1 . i) where x1 is Element of Bool [|M,M|] : x1 in X1  }  ) by A7, CLOSURE2:14, PBOOLE:def_1;
then consider z being Element of Bool [|M,M|] such that
A9: Z1 . i = z . i and
A10: z in X1 ;
reconsider z9 = z as Element of (EqRelLatt M) by A1, A10;
reconsider z1 = z9 as Equivalence_Relation of M by MSUALG_5:def_5;
 c [= z9 by A1, A6, A10, LATTICE3:def_16;
then  c9 c= z1 by Th6;
hence  c9 . i c= Z1 . i by A8, A9, PBOOLE:def_2; ::_thesis: verum
end;
hence  c9 c= Z1 by PBOOLE:def_2; ::_thesis: verum
end;
then  c9 c= meet |:X1:| by MSSUBFAM:45;
hence  c [= a9 by A3, Th6; ::_thesis: verum
end;
now__::_thesis:_for_q_being_Element_of_(EqRelLatt_M)_st_q_in_X_holds_
a9_[=_q
let q be Element of (EqRelLatt M); ::_thesis: ( q in X implies a9 [= q )
reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def_5;
assume  q in X ; ::_thesis: a9 [= q
then  a c= q9 by A1, A3, Th7;
hence  a9 [= q by Th6; ::_thesis: verum
end;
then  a9 is_less_than X by LATTICE3:def_16;
hence  a = b by A4, A5, LATTICE3:34; ::_thesis: verum
end;

begin

definition
let L be Lattice;
let IT be SubLattice of L;
attrIT is /\-inheriting  means :Def2: :: MSUALG_7:def 2
 for X being Subset of IT holds "/\" (X,L) in the carrier of IT;
attrIT is \/-inheriting  means :Def3: :: MSUALG_7:def 3
 for X being Subset of IT holds "\/" (X,L) in the carrier of IT;
end;

:: deftheorem Def2 defines /\-inheriting MSUALG_7:def_2_:_
 for L being Lattice
for IT being SubLattice of L holds
( IT is /\-inheriting iff for X being Subset of IT holds "/\" (X,L) in the carrier of IT );

:: deftheorem Def3 defines \/-inheriting MSUALG_7:def_3_:_
 for L being Lattice
for IT being SubLattice of L holds
( IT is \/-inheriting iff for X being Subset of IT holds "\/" (X,L) in the carrier of IT );

theorem Th11: :: MSUALG_7:11
for L being Lattice
for L9 being SubLattice of L
for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
proof
let L be Lattice; ::_thesis: for L9 being SubLattice of L
for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let L9 be SubLattice of L; ::_thesis: for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let a, b be Element of L; ::_thesis: for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let a9, b9 be Element of L9; ::_thesis: ( a = a9 & b = b9 implies ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) )
assume A1: ( a = a9 & b = b9 ) ; ::_thesis: ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
thus a "\/" b = the L_join of L . (a,b) by LATTICES:def_1
.= ( the L_join of L || the carrier of L9) . [a9,b9] by A1, FUNCT_1:49
.= the L_join of L9 . (a9,b9) by NAT_LAT:def_12
.= a9 "\/" b9 by LATTICES:def_1 ; ::_thesis: a "/\" b = a9 "/\" b9
thus a "/\" b = the L_meet of L . (a,b) by LATTICES:def_2
.= ( the L_meet of L || the carrier of L9) . [a9,b9] by A1, FUNCT_1:49
.= the L_meet of L9 . (a9,b9) by NAT_LAT:def_12
.= a9 "/\" b9 by LATTICES:def_2 ; ::_thesis: verum
end;

theorem Th12: :: MSUALG_7:12
for L being Lattice
for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )
proof
let L be Lattice; ::_thesis: for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )
let L9 be SubLattice of L; ::_thesis: for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )
let X be Subset of L9; ::_thesis: for a being Element of L
for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )
let a be Element of L; ::_thesis: for a9 being Element of L9 st a = a9 holds
( a is_less_than X iff a9 is_less_than X )
let a9 be Element of L9; ::_thesis: ( a = a9 implies ( a is_less_than X iff a9 is_less_than X ) )
assume A1: a = a9 ; ::_thesis: ( a is_less_than X iff a9 is_less_than X )
thus  ( a is_less_than X implies a9 is_less_than X ) ::_thesis: ( a9 is_less_than X implies a is_less_than X )
proof
assume A2: a is_less_than X ; ::_thesis: a9 is_less_than X
now__::_thesis:_for_q9_being_Element_of_L9_st_q9_in_X_holds_
a9_[=_q9
let q9 be Element of L9; ::_thesis: ( q9 in X implies a9 [= q9 )
 the carrier of L9 c= the carrier of L by NAT_LAT:def_12;
then reconsider q = q9 as Element of L by TARSKI:def_3;
assume  q9 in X ; ::_thesis: a9 [= q9
then A3: a [= q by A2, LATTICE3:def_16;
a9 "/\" q9 = a "/\" q by A1, Th11
.= a9 by A1, A3, LATTICES:4 ;
hence  a9 [= q9 by LATTICES:4; ::_thesis: verum
end;
hence  a9 is_less_than X by LATTICE3:def_16; ::_thesis: verum
end;
thus  ( a9 is_less_than X implies a is_less_than X ) ::_thesis: verum
proof
assume A4: a9 is_less_than X ; ::_thesis: a is_less_than X
now__::_thesis:_for_q_being_Element_of_L_st_q_in_X_holds_
a_[=_q
let q be Element of L; ::_thesis: ( q in X implies a [= q )
assume A5: q in X ; ::_thesis: a [= q
then reconsider q9 = q as Element of L9 ;
A6: a9 [= q9 by A4, A5, LATTICE3:def_16;
a "/\" q = a9 "/\" q9 by A1, Th11
.= a by A1, A6, LATTICES:4 ;
hence  a [= q by LATTICES:4; ::_thesis: verum
end;
hence  a is_less_than X by LATTICE3:def_16; ::_thesis: verum
end;
end;

theorem Th13: :: MSUALG_7:13
for L being Lattice
for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )
proof
let L be Lattice; ::_thesis: for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )
let L9 be SubLattice of L; ::_thesis: for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )
let X be Subset of L9; ::_thesis: for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )
let a be Element of L; ::_thesis: for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )
let a9 be Element of L9; ::_thesis: ( a = a9 implies ( X is_less_than a iff X is_less_than a9 ) )
assume A1: a = a9 ; ::_thesis: ( X is_less_than a iff X is_less_than a9 )
thus  ( X is_less_than a implies X is_less_than a9 ) ::_thesis: ( X is_less_than a9 implies X is_less_than a )
proof
assume A2: X is_less_than a ; ::_thesis: X is_less_than a9
now__::_thesis:_for_q9_being_Element_of_L9_st_q9_in_X_holds_
q9_[=_a9
let q9 be Element of L9; ::_thesis: ( q9 in X implies q9 [= a9 )
 the carrier of L9 c= the carrier of L by NAT_LAT:def_12;
then reconsider q = q9 as Element of L by TARSKI:def_3;
assume  q9 in X ; ::_thesis: q9 [= a9
then A3: q [= a by A2, LATTICE3:def_17;
q9 "/\" a9 = q "/\" a by A1, Th11
.= q9 by A3, LATTICES:4 ;
hence  q9 [= a9 by LATTICES:4; ::_thesis: verum
end;
hence  X is_less_than a9 by LATTICE3:def_17; ::_thesis: verum
end;
thus  ( X is_less_than a9 implies X is_less_than a ) ::_thesis: verum
proof
assume A4: X is_less_than a9 ; ::_thesis: X is_less_than a
now__::_thesis:_for_q_being_Element_of_L_st_q_in_X_holds_
q_[=_a
let q be Element of L; ::_thesis: ( q in X implies q [= a )
assume A5: q in X ; ::_thesis: q [= a
then reconsider q9 = q as Element of L9 ;
A6: q9 [= a9 by A4, A5, LATTICE3:def_17;
q "/\" a = q9 "/\" a9 by A1, Th11
.= q by A6, LATTICES:4 ;
hence  q [= a by LATTICES:4; ::_thesis: verum
end;
hence  X is_less_than a by LATTICE3:def_17; ::_thesis: verum
end;
end;

theorem Th14: :: MSUALG_7:14
for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
L9 is complete
proof
let L be complete Lattice; ::_thesis: for L9 being SubLattice of L st L9 is /\-inheriting holds
L9 is complete
let L9 be SubLattice of L; ::_thesis: ( L9 is /\-inheriting implies L9 is complete )
assume A1: L9 is /\-inheriting ; ::_thesis: L9 is complete
 for X being Subset of L9 ex a being Element of L9 st
( a is_less_than X & ( for b being Element of L9 st b is_less_than X holds
b [= a ) )
proof
let X be Subset of L9; ::_thesis: ex a being Element of L9 st
( a is_less_than X & ( for b being Element of L9 st b is_less_than X holds
b [= a ) )
set a = "/\" (X,L);
reconsider a9 = "/\" (X,L) as Element of L9 by A1, Def2;
take  a9 ; ::_thesis: ( a9 is_less_than X & ( for b being Element of L9 st b is_less_than X holds
b [= a9 ) )
 "/\" (X,L) is_less_than X by LATTICE3:34;
hence  a9 is_less_than X by Th12; ::_thesis: for b being Element of L9 st b is_less_than X holds
b [= a9
let b9 be Element of L9; ::_thesis: ( b9 is_less_than X implies b9 [= a9 )
 the carrier of L9 c= the carrier of L by NAT_LAT:def_12;
then reconsider b = b9 as Element of L by TARSKI:def_3;
assume  b9 is_less_than X ; ::_thesis: b9 [= a9
then  b is_less_than X by Th12;
then A2: b [= "/\" (X,L) by LATTICE3:39;
b9 "/\" a9 = b "/\" ("/\" (X,L)) by Th11
.= b9 by A2, LATTICES:4 ;
hence  b9 [= a9 by LATTICES:4; ::_thesis: verum
end;
hence  L9 is complete by VECTSP_8:def_6; ::_thesis: verum
end;

theorem Th15: :: MSUALG_7:15
for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
L9 is complete
proof
let L be complete Lattice; ::_thesis: for L9 being SubLattice of L st L9 is \/-inheriting holds
L9 is complete
let L9 be SubLattice of L; ::_thesis: ( L9 is \/-inheriting implies L9 is complete )
assume A1: L9 is \/-inheriting ; ::_thesis: L9 is complete
 for X being Subset of L9 ex a being Element of L9 st
( X is_less_than a & ( for b being Element of L9 st X is_less_than b holds
a [= b ) )
proof
let X be Subset of L9; ::_thesis: ex a being Element of L9 st
( X is_less_than a & ( for b being Element of L9 st X is_less_than b holds
a [= b ) )
set a = "\/" (X,L);
reconsider a9 = "\/" (X,L) as Element of L9 by A1, Def3;
take  a9 ; ::_thesis: ( X is_less_than a9 & ( for b being Element of L9 st X is_less_than b holds
a9 [= b ) )
 X is_less_than "\/" (X,L) by LATTICE3:def_21;
hence  X is_less_than a9 by Th13; ::_thesis: for b being Element of L9 st X is_less_than b holds
a9 [= b
let b9 be Element of L9; ::_thesis: ( X is_less_than b9 implies a9 [= b9 )
 the carrier of L9 c= the carrier of L by NAT_LAT:def_12;
then reconsider b = b9 as Element of L by TARSKI:def_3;
assume  X is_less_than b9 ; ::_thesis: a9 [= b9
then  X is_less_than b by Th13;
then A2: "\/" (X,L) [= b by LATTICE3:def_21;
a9 "/\" b9 = ("\/" (X,L)) "/\" b by Th11
.= a9 by A2, LATTICES:4 ;
hence  a9 [= b9 by LATTICES:4; ::_thesis: verum
end;
hence  L9 is complete by Def1; ::_thesis: verum
end;

registration
let L be complete Lattice;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete for SubLattice of L;
existence
 ex b1 being SubLattice of L st b1 is complete
proof
reconsider L1 = L as SubLattice of L by NAT_LAT:15;
take  L1 ; ::_thesis: L1 is complete
thus  L1 is complete ; ::_thesis: verum
end;
end;

registration
let L be complete Lattice;
cluster /\-inheriting  ->  complete for SubLattice of L;
coherence
 for b1 being SubLattice of L st b1 is /\-inheriting holds
b1 is complete by Th14;
cluster \/-inheriting  ->  complete for SubLattice of L;
coherence
 for b1 being SubLattice of L st b1 is \/-inheriting holds
b1 is complete by Th15;
end;

theorem Th16: :: MSUALG_7:16
for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9)
proof
let L be complete Lattice; ::_thesis: for L9 being SubLattice of L st L9 is /\-inheriting holds
for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9)
let L9 be SubLattice of L; ::_thesis: ( L9 is /\-inheriting implies for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9) )
assume A1: L9 is /\-inheriting ; ::_thesis: for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9)
then reconsider L91 = L9 as complete SubLattice of L ;
let A9 be Subset of L9; ::_thesis: "/\" (A9,L) = "/\" (A9,L9)
set a = "/\" (A9,L);
reconsider a9 = "/\" (A9,L) as Element of L91 by A1, Def2;
A2: now__::_thesis:_for_c9_being_Element_of_L91_st_c9_is_less_than_A9_holds_
c9_[=_a9
let c9 be Element of L91; ::_thesis: ( c9 is_less_than A9 implies c9 [= a9 )
 the carrier of L91 c= the carrier of L by NAT_LAT:def_12;
then reconsider c = c9 as Element of L by TARSKI:def_3;
assume  c9 is_less_than A9 ; ::_thesis: c9 [= a9
then  c is_less_than A9 by Th12;
then A3: c [= "/\" (A9,L) by LATTICE3:34;
c9 "/\" a9 = c "/\" ("/\" (A9,L)) by Th11
.= c9 by A3, LATTICES:4 ;
hence  c9 [= a9 by LATTICES:4; ::_thesis: verum
end;
 "/\" (A9,L) is_less_than A9 by LATTICE3:34;
then  a9 is_less_than A9 by Th12;
hence  "/\" (A9,L) = "/\" (A9,L9) by A2, LATTICE3:34; ::_thesis: verum
end;

theorem Th17: :: MSUALG_7:17
for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)
proof
let L be complete Lattice; ::_thesis: for L9 being SubLattice of L st L9 is \/-inheriting holds
for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)
let L9 be SubLattice of L; ::_thesis: ( L9 is \/-inheriting implies for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9) )
assume A1: L9 is \/-inheriting ; ::_thesis: for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)
then reconsider L91 = L9 as complete SubLattice of L ;
let A9 be Subset of L9; ::_thesis: "\/" (A9,L) = "\/" (A9,L9)
set a = "\/" (A9,L);
reconsider a9 = "\/" (A9,L) as Element of L91 by A1, Def3;
A2: now__::_thesis:_for_c9_being_Element_of_L91_st_A9_is_less_than_c9_holds_
a9_[=_c9
let c9 be Element of L91; ::_thesis: ( A9 is_less_than c9 implies a9 [= c9 )
 the carrier of L91 c= the carrier of L by NAT_LAT:def_12;
then reconsider c = c9 as Element of L by TARSKI:def_3;
assume  A9 is_less_than c9 ; ::_thesis: a9 [= c9
then  A9 is_less_than c by Th13;
then A3: "\/" (A9,L) [= c by LATTICE3:def_21;
a9 "/\" c9 = ("\/" (A9,L)) "/\" c by Th11
.= a9 by A3, LATTICES:4 ;
hence  a9 [= c9 by LATTICES:4; ::_thesis: verum
end;
 A9 is_less_than "\/" (A9,L) by LATTICE3:def_21;
then  A9 is_less_than a9 by Th13;
hence  "\/" (A9,L) = "\/" (A9,L9) by A2, LATTICE3:def_21; ::_thesis: verum
end;

theorem :: MSUALG_7:18
for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
for A being Subset of L
for A9 being Subset of L9 st A = A9 holds
"/\" A = "/\" A9 by Th16;

theorem :: MSUALG_7:19
for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
for A being Subset of L
for A9 being Subset of L9 st A = A9 holds
"\/" A = "\/" A9 by Th17;

begin

definition
let r1, r2 be Real;
assume A1: r1 <= r2 ;
func RealSubLatt (r1,r2) ->  strict Lattice means :Def4: :: MSUALG_7:def 4
( the carrier of it = [.r1,r2.] & the L_join of it = maxreal || [.r1,r2.] & the L_meet of it = minreal || [.r1,r2.] );
existence
 ex b1 being strict Lattice st
( the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] )
proof
 r2 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A1;
then reconsider A = [.r1,r2.] as non empty set by RCOMP_1:def_1;
 [:A,A:] c= [:REAL,REAL:] by ZFMISC_1:96;
then reconsider Ma = maxreal || A, Mi = minreal || A as Function of [:A,A:],REAL by FUNCT_2:32;
A1: dom Mi = [:A,A:] by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_Mi_holds_
Mi_._x_in_A
let x be set ; ::_thesis: ( x in dom Mi implies Mi . x in A )
assume A3: x in dom Mi ; ::_thesis: Mi . x in A
then consider x1, x2 being set  such that
A4: x = [x1,x2] by RELAT_1:def_1;
 x2 in A by A3, A4, ZFMISC_1:87;
then  x2 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then consider y2 being Element of REAL  such that
A5: x2 = y2 and
A6: ( r1 <= y2 & y2 <= r2 ) ;
 x1 in A by A3, A4, ZFMISC_1:87;
then  x1 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then consider y1 being Element of REAL  such that
A7: x1 = y1 and
A8: ( r1 <= y1 & y1 <= r2 ) ;
Mi . x = minreal . (x1,x2) by A3, A4, FUNCT_1:49
.= min (y1,y2) by A7, A5, REAL_LAT:def_1 ;
then  ( Mi . x = y1 or Mi . x = y2 ) by XXREAL_0:15;
then  Mi . x in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A8, A6;
hence  Mi . x in A by RCOMP_1:def_1; ::_thesis: verum
end;
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_Ma_holds_
Ma_._x_in_A
let x be set ; ::_thesis: ( x in dom Ma implies Ma . x in A )
assume A10: x in dom Ma ; ::_thesis: Ma . x in A
then consider x1, x2 being set  such that
A11: x = [x1,x2] by RELAT_1:def_1;
 x2 in A by A10, A11, ZFMISC_1:87;
then  x2 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then consider y2 being Element of REAL  such that
A12: x2 = y2 and
A13: ( r1 <= y2 & y2 <= r2 ) ;
 x1 in A by A10, A11, ZFMISC_1:87;
then  x1 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then consider y1 being Element of REAL  such that
A14: x1 = y1 and
A15: ( r1 <= y1 & y1 <= r2 ) ;
Ma . x = maxreal . (x1,x2) by A10, A11, FUNCT_1:49
.= max (y1,y2) by A14, A12, REAL_LAT:def_2 ;
then  ( Ma . x = y1 or Ma . x = y2 ) by XXREAL_0:16;
then  Ma . x in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A15, A13;
hence  Ma . x in A by RCOMP_1:def_1; ::_thesis: verum
end;
reconsider Mi = Mi as BinOp of A by A1, A2, FUNCT_2:3;
 dom Ma = [:A,A:] by FUNCT_2:def_1;
then reconsider Ma = Ma as BinOp of A by A9, FUNCT_2:3;
set R = Real_Lattice ;
set L9 = LattStr(# A,Ma,Mi #);
reconsider L = LattStr(# A,Ma,Mi #) as non empty LattStr ;
A16: now__::_thesis:_for_a,_b_being_Element_of_L_holds_
(_a_"\/"_b_=_maxreal_._(a,b)_&_a_"/\"_b_=_minreal_._(a,b)_)
let a, b be Element of L; ::_thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
thus a "\/" b = the L_join of L . (a,b) by LATTICES:def_1
.= maxreal . [a,b] by FUNCT_1:49
.= maxreal . (a,b) ; ::_thesis: a "/\" b = minreal . (a,b)
thus a "/\" b = the L_meet of L . (a,b) by LATTICES:def_2
.= minreal . [a,b] by FUNCT_1:49
.= minreal . (a,b) ; ::_thesis: verum
end;
A17: now__::_thesis:_for_x_being_Element_of_A_holds_x_is_Element_of_Real_Lattice
let x be Element of A; ::_thesis: x is Element of Real_Lattice
 x in A ;
then  x in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then  ex y being Element of REAL st
( x = y & r1 <= y & y <= r2 ) ;
hence  x is Element of Real_Lattice by REAL_LAT:def_3; ::_thesis: verum
end;
A18: now__::_thesis:_for_p,_q_being_Element_of_L_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of L; ::_thesis: p "\/" q = q "\/" p
reconsider p9 = p, q9 = q as Element of Real_Lattice by A17;
thus p "\/" q = maxreal . (p,q) by A16
.= maxreal . (q9,p9) by REAL_LAT:1
.= q "\/" p by A16 ; ::_thesis: verum
end;
A19: now__::_thesis:_for_p,_q_being_Element_of_L_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of L; ::_thesis: p "/\" (p "\/" q) = p
reconsider p9 = p, q9 = q as Element of Real_Lattice by A17;
thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A16
.= minreal . (p9,(maxreal . (p9,q9))) by A16
.= p by REAL_LAT:6 ; ::_thesis: verum
end;
A20: now__::_thesis:_for_p,_q_being_Element_of_L_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of L; ::_thesis: p "/\" q = q "/\" p
reconsider p9 = p, q9 = q as Element of Real_Lattice by A17;
thus p "/\" q = minreal . (p,q) by A16
.= minreal . (q9,p9) by REAL_LAT:2
.= q "/\" p by A16 ; ::_thesis: verum
end;
A21: now__::_thesis:_for_p,_q_being_Element_of_L_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of L; ::_thesis: (p "/\" q) "\/" q = q
reconsider p9 = p, q9 = q as Element of Real_Lattice by A17;
thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A16
.= maxreal . ((minreal . (p9,q9)),q9) by A16
.= q by REAL_LAT:5 ; ::_thesis: verum
end;
A22: now__::_thesis:_for_p,_q,_r_being_Element_of_L_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of L; ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A17;
thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A16
.= minreal . (p,(minreal . (q,r))) by A16
.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4
.= minreal . ((p "/\" q),r) by A16
.= (p "/\" q) "/\" r by A16 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_L_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of L; ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A17;
thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A16
.= maxreal . (p,(maxreal . (q,r))) by A16
.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3
.= maxreal . ((p "\/" q),r) by A16
.= (p "\/" q) "\/" r by A16 ; ::_thesis: verum
end;
then  ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A18, A21, A20, A22, A19, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L9 = LattStr(# A,Ma,Mi #) as strict Lattice ;
take  L9 ; ::_thesis: ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] )
thus  ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Lattice st the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] & the carrier of b2 = [.r1,r2.] & the L_join of b2 = maxreal || [.r1,r2.] & the L_meet of b2 = minreal || [.r1,r2.] holds
b1 = b2 ;
end;

:: deftheorem Def4 defines RealSubLatt MSUALG_7:def_4_:_
 for r1, r2 being Real st r1 <= r2 holds
for b3 being strict Lattice holds
( b3 = RealSubLatt (r1,r2) iff ( the carrier of b3 = [.r1,r2.] & the L_join of b3 = maxreal || [.r1,r2.] & the L_meet of b3 = minreal || [.r1,r2.] ) );

theorem Th20: :: MSUALG_7:20
for r1, r2 being Real st r1 <= r2 holds
RealSubLatt (r1,r2) is complete
proof
let r1, r2 be Real; ::_thesis: ( r1 <= r2 implies RealSubLatt (r1,r2) is complete )
assume A1: r1 <= r2 ; ::_thesis: RealSubLatt (r1,r2) is complete
reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def_1;
set A = [.r1,r2.];
set L9 = RealSubLatt (r1,r2);
A2: the carrier of (RealSubLatt (r1,r2)) = [.r1,r2.] by A1, Def4;
A3: the L_meet of (RealSubLatt (r1,r2)) = minreal || [.r1,r2.] by A1, Def4;
now__::_thesis:_for_X_being_Subset_of_(RealSubLatt_(r1,r2))_ex_a_being_Element_of_(RealSubLatt_(r1,r2))_st_
(_a_is_less_than_X_&_(_for_b_being_Element_of_(RealSubLatt_(r1,r2))_st_b_is_less_than_X_holds_
b_[=_a_)_)
let X be Subset of (RealSubLatt (r1,r2)); ::_thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )
percases ( X is empty or not X is empty ) ;
supposeA4: X is empty ; ::_thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )
thus  ex a being Element of (RealSubLatt (r1,r2)) st
( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) ) ::_thesis: verum
proof
 r2 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A1;
then reconsider a = r2 as Element of (RealSubLatt (r1,r2)) by A2, RCOMP_1:def_1;
take  a ; ::_thesis: ( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) )
 for q being Element of (RealSubLatt (r1,r2)) st q in X holds
a [= q by A4;
hence  a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a
let b be Element of (RealSubLatt (r1,r2)); ::_thesis: ( b is_less_than X implies b [= a )
assume  b is_less_than X ; ::_thesis: b [= a
A5: b in [.r1,r2.] by A2;
then reconsider b9 = b as Element of REAL ;
 b in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A5, RCOMP_1:def_1;
then A6: ex b1 being Element of REAL st
( b = b1 & r1 <= b1 & b1 <= r2 ) ;
b "/\" a = (minreal || [.r1,r2.]) . (b,a) by A3, LATTICES:def_2
.= minreal . [b,a] by A2, FUNCT_1:49
.= minreal . (b,a)
.= min (b9,r2) by REAL_LAT:def_1
.= b by A6, XXREAL_0:def_9 ;
hence  b [= a by LATTICES:4; ::_thesis: verum
end;
end;
supposeA7: not X is empty ; ::_thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )
 X c= REAL by A2, XBOOLE_1:1;
then reconsider X1 = X as non empty Subset of ExtREAL by A7, NUMBERS:31, XBOOLE_1:1;
thus  ex a being Element of (RealSubLatt (r1,r2)) st
( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) ) ::_thesis: verum
proof
set g = the Element of X1;
set A1 = inf X1;
set LB = r1 - 1;
 r1 - 1 is LowerBound of X1
proof
let v be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not v in X1 or r1 - 1 <= v )
assume  v in X1 ; ::_thesis: r1 - 1 <= v
then  v in the carrier of (RealSubLatt (r1,r2)) ;
then  v in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A2, RCOMP_1:def_1;
then consider w being Element of REAL  such that
A8: v = w and
A9: r1 <= w and
 w <= r2 ;
 r1 - 1 <= r1 - 0 by XREAL_1:13;
then  (r1 - 1) + r1 <= r1 + w by A9, XREAL_1:7;
hence  r1 - 1 <= v by A8, XREAL_1:6; ::_thesis: verum
end;
then A10: X1 is bounded_below by XXREAL_2:def_9;
 X <> {+infty}
proof
assume  X = {+infty} ; ::_thesis: contradiction
then  +infty in X by TARSKI:def_1;
hence  contradiction by A2; ::_thesis: verum
end;
then A11: inf X1 is Real by A10, XXREAL_2:58;
 the Element of X1 in [.r1,r2.] by A2, TARSKI:def_3;
then  the Element of X1 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then A12: ex w being Element of REAL st
( the Element of X1 = w & r1 <= w & w <= r2 ) ;
A13: inf X1 is LowerBound of X1 by XXREAL_2:def_4;
then  inf X1 <= the Element of X1 by XXREAL_2:def_2;
then consider A9, R29 being Real such that
A14: A9 = inf X1 and
A15: ( R29 = R2 & A9 <= R29 ) by A11, A12, XXREAL_0:2;
now__::_thesis:_for_v_being_ext-real_number_st_v_in_X1_holds_
R1_<=_v
let v be ext-real number ; ::_thesis: ( v in X1 implies R1 <= v )
assume  v in X1 ; ::_thesis: R1 <= v
then  v in [.r1,r2.] by A2;
then  v in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by RCOMP_1:def_1;
then  ex w being Element of REAL st
( v = w & r1 <= w & w <= r2 ) ;
hence  R1 <= v ; ::_thesis: verum
end;
then  R1 is LowerBound of X1 by XXREAL_2:def_2;
then  R1 <= inf X1 by XXREAL_2:def_4;
then  A9 in  {  r where r is Real : ( r1 <= r & r <= r2 )  }  by A14, A15;
then reconsider a = inf X1 as Element of (RealSubLatt (r1,r2)) by A2, A14, RCOMP_1:def_1;
take  a ; ::_thesis: ( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) )
 a in [.r1,r2.] by A2;
then reconsider a9 = a as Element of REAL ;
now__::_thesis:_for_q_being_Element_of_(RealSubLatt_(r1,r2))_st_q_in_X_holds_
a_[=_q
let q be Element of (RealSubLatt (r1,r2)); ::_thesis: ( q in X implies a [= q )
assume A16: q in X ; ::_thesis: a [= q
 q in [.r1,r2.] by A2;
then reconsider q9 = q as Element of REAL ;
 q9 in REAL ;
then reconsider Q = q9 as R_eal by NUMBERS:31;
 inf X1 = a9 ;
then A17: ex a1, q1 being Real st
( a1 = inf X1 & q1 = Q & a1 <= q1 ) by A13, A16, XXREAL_2:def_2;
a "/\" q = (minreal || [.r1,r2.]) . (a,q) by A3, LATTICES:def_2
.= minreal . [a,q] by A2, FUNCT_1:49
.= minreal . (a,q)
.= min (a9,q9) by REAL_LAT:def_1
.= a by A17, XXREAL_0:def_9 ;
hence  a [= q by LATTICES:4; ::_thesis: verum
end;
hence  a is_less_than X by LATTICE3:def_16; ::_thesis: for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a
let b be Element of (RealSubLatt (r1,r2)); ::_thesis: ( b is_less_than X implies b [= a )
 b in [.r1,r2.] by A2;
then reconsider b9 = b as Element of REAL ;
 b9 in REAL ;
then reconsider B = b9 as R_eal by NUMBERS:31;
assume A18: b is_less_than X ; ::_thesis: b [= a
now__::_thesis:_for_h_being_ext-real_number_st_h_in_X_holds_
B_<=_h
let h be ext-real number ; ::_thesis: ( h in X implies B <= h )
assume A19: h in X ; ::_thesis: B <= h
then reconsider h1 = h as Element of (RealSubLatt (r1,r2)) ;
 h in [.r1,r2.] by A2, A19;
then reconsider h9 = h as Real ;
A20: b [= h1 by A18, A19, LATTICE3:def_16;
min (b9,h9) = minreal . (b,h1) by REAL_LAT:def_1
.= (minreal || [.r1,r2.]) . [b,h1] by A2, FUNCT_1:49
.= (minreal || [.r1,r2.]) . (b,h1)
.= b "/\" h1 by A3, LATTICES:def_2
.= b9 by A20, LATTICES:4 ;
hence  B <= h by XXREAL_0:def_9; ::_thesis: verum
end;
then  B is LowerBound of X1 by XXREAL_2:def_2;
then A21: B <= inf X1 by XXREAL_2:def_4;
b "/\" a = (minreal || [.r1,r2.]) . (b,a) by A3, LATTICES:def_2
.= minreal . [b,a] by A2, FUNCT_1:49
.= minreal . (b,a)
.= min (b9,a9) by REAL_LAT:def_1
.= b by A21, XXREAL_0:def_9 ;
hence  b [= a by LATTICES:4; ::_thesis: verum
end;
end;
end;
end;
hence  RealSubLatt (r1,r2) is complete by VECTSP_8:def_6; ::_thesis: verum
end;

theorem Th21: :: MSUALG_7:21
ex L9 being SubLattice of RealSubLatt (0,1) st
( L9 is \/-inheriting & not L9 is /\-inheriting )
proof
set B = {0,1} \/ ].(1 / 2),1.[;
set L = RealSubLatt (0,1);
set R = Real_Lattice ;
A1: {0,1} \/ ].(1 / 2),1.[ c= {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {0,1} \/ ].(1 / 2),1.[ or x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  )
assume A2: x1 in {0,1} \/ ].(1 / 2),1.[ ; ::_thesis: x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }
now__::_thesis:_x1_in_{0}_\/__{__x_where_x_is_Element_of_REAL_:_(_1_/_2_<_x_&_x_<=_1_)__}_
percases ( x1 in {0,1} or x1 in ].(1 / 2),1.[ ) by A2, XBOOLE_0:def_3;
suppose x1 in {0,1} ; ::_thesis: x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }
then  ( x1 = 0 or x1 = 1 ) by TARSKI:def_2;
then  ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by TARSKI:def_1;
hence  x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x1 in ].(1 / 2),1.[ ; ::_thesis: x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }
then  x1 in  {  r where r is Real : ( 1 / 2 < r & r < 1 )  }  by RCOMP_1:def_2;
then consider y being Element of REAL  such that
A3: x1 = y and
A4: ( 1 / 2 < y & y < 1 ) ;
 y in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A4;
hence  x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: verum
end;
 {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  c= {0,1} \/ ].(1 / 2),1.[
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  or x1 in {0,1} \/ ].(1 / 2),1.[ )
assume A5: x1 in {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: x1 in {0,1} \/ ].(1 / 2),1.[
now__::_thesis:_x1_in_{0,1}_\/_].(1_/_2),1.[
percases ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A5, XBOOLE_0:def_3;
suppose x1 in {0} ; ::_thesis: x1 in {0,1} \/ ].(1 / 2),1.[
then  x1 = 0 by TARSKI:def_1;
then  x1 in {0,1} by TARSKI:def_2;
hence  x1 in {0,1} \/ ].(1 / 2),1.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: x1 in {0,1} \/ ].(1 / 2),1.[
then consider y being Element of REAL  such that
A6: x1 = y and
A7: 1 / 2 < y and
A8: y <= 1 ;
 ( y < 1 or y = 1 ) by A8, XXREAL_0:1;
then  ( y in  {  r where r is Real : ( 1 / 2 < r & r < 1 )  }  or y = 1 ) by A7;
then  ( y in ].(1 / 2),1.[ or y in {0,1} ) by RCOMP_1:def_2, TARSKI:def_2;
hence  x1 in {0,1} \/ ].(1 / 2),1.[ by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x1 in {0,1} \/ ].(1 / 2),1.[ ; ::_thesis: verum
end;
then A9: {0,1} \/ ].(1 / 2),1.[ = {0} \/  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A1, XBOOLE_0:def_10;
A10: 0 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
then reconsider A = [.0,1.] as non empty set by RCOMP_1:def_1;
A11: the L_meet of (RealSubLatt (0,1)) = minreal || [.0,1.] by Def4;
reconsider B = {0,1} \/ ].(1 / 2),1.[ as non empty set ;
A12: the L_join of (RealSubLatt (0,1)) = maxreal || [.0,1.] by Def4;
A13: A = the carrier of (RealSubLatt (0,1)) by Def4;
then reconsider Ma = maxreal || A, Mi = minreal || A as BinOp of A by Def4;
A14: now__::_thesis:_for_x1_being_set_st_x1_in_B_holds_
x1_in_A
let x1 be set ; ::_thesis: ( x1 in B implies x1 in A )
assume A15: x1 in B ; ::_thesis: x1 in A
now__::_thesis:_x1_in_A
percases ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A15, XBOOLE_0:def_3;
suppose x1 in {0} ; ::_thesis: x1 in A
then  x1 = 0 by TARSKI:def_1;
hence  x1 in A by A10, RCOMP_1:def_1; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: x1 in A
then  ex y being Element of REAL st
( x1 = y & 1 / 2 < y & y <= 1 ) ;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
hence  x1 in A by RCOMP_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x1 in A ; ::_thesis: verum
end;
then A16: B c= A by TARSKI:def_3;
then A17: [:B,B:] c= [:A,A:] by ZFMISC_1:96;
then reconsider ma = Ma || B, mi = Mi || B as Function of [:B,B:],A by FUNCT_2:32;
A18: now__::_thesis:_for_x1_being_Element_of_A_holds_x1_is_Element_of_Real_Lattice
let x1 be Element of A; ::_thesis: x1 is Element of Real_Lattice
 x1 in A ;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then  ex y1 being Element of REAL st
( x1 = y1 & 0 <= y1 & y1 <= 1 ) ;
hence  x1 is Element of Real_Lattice by REAL_LAT:def_3; ::_thesis: verum
end;
A19: dom mi = [:B,B:] by FUNCT_2:def_1;
A20: now__::_thesis:_for_x9_being_set_st_x9_in_dom_mi_holds_
mi_._x9_in_B
let x9 be set ; ::_thesis: ( x9 in dom mi implies mi . x9 in B )
assume A21: x9 in dom mi ; ::_thesis: mi . x9 in B
then consider x1, x2 being set  such that
A22: x9 = [x1,x2] by RELAT_1:def_1;
A23: x2 in B by A21, A22, ZFMISC_1:87;
A24: x1 in B by A21, A22, ZFMISC_1:87;
now__::_thesis:_mi_._x9_in_B
percases ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A24, XBOOLE_0:def_3;
suppose x1 in {0} ; ::_thesis: mi . x9 in B
then A25: x1 = 0 by TARSKI:def_1;
now__::_thesis:_mi_._x9_in_B
percases ( x2 in {0} or x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A23, XBOOLE_0:def_3;
suppose x2 in {0} ; ::_thesis: mi . x9 in B
then A26: x2 = 0 by TARSKI:def_1;
mi . x9 = Mi . [x1,x2] by A21, A22, FUNCT_1:49
.= minreal . (x1,x2) by A17, A19, A21, A22, FUNCT_1:49
.= min (0,0) by A25, A26, REAL_LAT:def_1
.= 0 ;
then  mi . x9 in {0} by TARSKI:def_1;
hence  mi . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: mi . x9 in B
then consider y2 being Element of REAL  such that
A27: x2 = y2 and
A28: ( 1 / 2 < y2 & y2 <= 1 ) ;
mi . x9 = Mi . [x1,x2] by A21, A22, FUNCT_1:49
.= minreal . (x1,x2) by A17, A19, A21, A22, FUNCT_1:49
.= min (0,y2) by A25, A27, REAL_LAT:def_1 ;
then  ( mi . x9 = 0 or mi . x9 = y2 ) by XXREAL_0:15;
then  ( mi . x9 in {0} or mi . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A28, TARSKI:def_1;
hence  mi . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: mi . x9 in B
then consider y1 being Element of REAL  such that
A29: x1 = y1 and
A30: ( 1 / 2 < y1 & y1 <= 1 ) ;
now__::_thesis:_mi_._x9_in_B
percases ( x2 in {0} or x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A23, XBOOLE_0:def_3;
suppose x2 in {0} ; ::_thesis: mi . x9 in B
then A31: x2 = 0 by TARSKI:def_1;
mi . x9 = Mi . [x1,x2] by A21, A22, FUNCT_1:49
.= minreal . (x1,x2) by A17, A19, A21, A22, FUNCT_1:49
.= min (y1,0) by A29, A31, REAL_LAT:def_1 ;
then  ( mi . x9 = y1 or mi . x9 = 0 ) by XXREAL_0:15;
then  ( mi . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  or mi . x9 in {0} ) by A30, TARSKI:def_1;
hence  mi . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: mi . x9 in B
then consider y2 being Element of REAL  such that
A32: x2 = y2 and
A33: ( 1 / 2 < y2 & y2 <= 1 ) ;
mi . x9 = Mi . [x1,x2] by A21, A22, FUNCT_1:49
.= minreal . (x1,x2) by A17, A19, A21, A22, FUNCT_1:49
.= min (y1,y2) by A29, A32, REAL_LAT:def_1 ;
then  ( mi . x9 = y1 or mi . x9 = y2 ) by XXREAL_0:15;
then  mi . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A30, A33;
hence  mi . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
A34: dom ma = [:B,B:] by FUNCT_2:def_1;
A35: now__::_thesis:_for_x9_being_set_st_x9_in_dom_ma_holds_
ma_._x9_in_B
let x9 be set ; ::_thesis: ( x9 in dom ma implies ma . x9 in B )
assume A36: x9 in dom ma ; ::_thesis: ma . x9 in B
then consider x1, x2 being set  such that
A37: x9 = [x1,x2] by RELAT_1:def_1;
A38: x2 in B by A36, A37, ZFMISC_1:87;
A39: x1 in B by A36, A37, ZFMISC_1:87;
now__::_thesis:_ma_._x9_in_B
percases ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A39, XBOOLE_0:def_3;
suppose x1 in {0} ; ::_thesis: ma . x9 in B
then A40: x1 = 0 by TARSKI:def_1;
now__::_thesis:_ma_._x9_in_B
percases ( x2 in {0} or x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A38, XBOOLE_0:def_3;
suppose x2 in {0} ; ::_thesis: ma . x9 in B
then A41: x2 = 0 by TARSKI:def_1;
ma . x9 = Ma . [x1,x2] by A36, A37, FUNCT_1:49
.= maxreal . (x1,x2) by A17, A34, A36, A37, FUNCT_1:49
.= max (0,0) by A40, A41, REAL_LAT:def_2
.= 0 ;
then  ma . x9 in {0} by TARSKI:def_1;
hence  ma . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: ma . x9 in B
then consider y2 being Element of REAL  such that
A42: x2 = y2 and
A43: ( 1 / 2 < y2 & y2 <= 1 ) ;
ma . x9 = Ma . [x1,x2] by A36, A37, FUNCT_1:49
.= maxreal . (x1,x2) by A17, A34, A36, A37, FUNCT_1:49
.= max (0,y2) by A40, A42, REAL_LAT:def_2 ;
then  ( ma . x9 = 0 or ma . x9 = y2 ) by XXREAL_0:16;
then  ( ma . x9 in {0} or ma . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A43, TARSKI:def_1;
hence  ma . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: ma . x9 in B
then consider y1 being Element of REAL  such that
A44: x1 = y1 and
A45: ( 1 / 2 < y1 & y1 <= 1 ) ;
now__::_thesis:_ma_._x9_in_B
percases ( x2 in {0} or x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A1, A38, XBOOLE_0:def_3;
suppose x2 in {0} ; ::_thesis: ma . x9 in B
then A46: x2 = 0 by TARSKI:def_1;
ma . x9 = Ma . [x1,x2] by A36, A37, FUNCT_1:49
.= maxreal . (x1,x2) by A17, A34, A36, A37, FUNCT_1:49
.= max (y1,0) by A44, A46, REAL_LAT:def_2 ;
then  ( ma . x9 = y1 or ma . x9 = 0 ) by XXREAL_0:16;
then  ( ma . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  or ma . x9 in {0} ) by A45, TARSKI:def_1;
hence  ma . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: ma . x9 in B
then consider y2 being Element of REAL  such that
A47: x2 = y2 and
A48: ( 1 / 2 < y2 & y2 <= 1 ) ;
ma . x9 = Ma . [x1,x2] by A36, A37, FUNCT_1:49
.= maxreal . (x1,x2) by A17, A34, A36, A37, FUNCT_1:49
.= max (y1,y2) by A44, A47, REAL_LAT:def_2 ;
then  ( ma . x9 = y1 or ma . x9 = y2 ) by XXREAL_0:16;
then  ma . x9 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A45, A48;
hence  ma . x9 in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
reconsider mi = mi as BinOp of B by A19, A20, FUNCT_2:3;
reconsider ma = ma as BinOp of B by A34, A35, FUNCT_2:3;
reconsider L9 = LattStr(# B,ma,mi #) as non empty LattStr ;
A49: now__::_thesis:_for_a,_b_being_Element_of_L9_holds_
(_a_"\/"_b_=_maxreal_._(a,b)_&_a_"/\"_b_=_minreal_._(a,b)_)
let a, b be Element of L9; ::_thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
A50: [a,b] in [:B,B:] ;
thus a "\/" b = the L_join of L9 . (a,b) by LATTICES:def_1
.= (maxreal || A) . [a,b] by FUNCT_1:49
.= maxreal . (a,b) by A17, A50, FUNCT_1:49 ; ::_thesis: a "/\" b = minreal . (a,b)
thus a "/\" b = the L_meet of L9 . (a,b) by LATTICES:def_2
.= (minreal || A) . [a,b] by FUNCT_1:49
.= minreal . (a,b) by A17, A50, FUNCT_1:49 ; ::_thesis: verum
end;
reconsider L = RealSubLatt (0,1) as complete Lattice by Th20;
A51: now__::_thesis:_for_x1_being_Element_of_B_holds_x1_is_Element_of_L
let x1 be Element of B; ::_thesis: x1 is Element of L
now__::_thesis:_x1_is_Element_of_L
percases ( x1 in {0} or x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by A9, XBOOLE_0:def_3;
suppose x1 in {0} ; ::_thesis: x1 is Element of L
then  x1 = 0 by TARSKI:def_1;
hence  x1 is Element of L by A10, A13, RCOMP_1:def_1; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ; ::_thesis: x1 is Element of L
then  ex y being Element of REAL st
( x1 = y & 1 / 2 < y & y <= 1 ) ;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
hence  x1 is Element of L by A13, RCOMP_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x1 is Element of L ; ::_thesis: verum
end;
A52: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of L9; ::_thesis: p "\/" q = q "\/" p
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A18;
thus p "\/" q = maxreal . (p,q) by A49
.= maxreal . (q9,p9) by REAL_LAT:1
.= q "\/" p by A49 ; ::_thesis: verum
end;
A53: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of L9; ::_thesis: p "/\" (p "\/" q) = p
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A18;
thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A49
.= minreal . (p9,(maxreal . (p9,q9))) by A49
.= p by REAL_LAT:6 ; ::_thesis: verum
end;
A54: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of L9; ::_thesis: p "/\" q = q "/\" p
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A18;
thus p "/\" q = minreal . (p,q) by A49
.= minreal . (q9,p9) by REAL_LAT:2
.= q "/\" p by A49 ; ::_thesis: verum
end;
A55: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of L9; ::_thesis: (p "/\" q) "\/" q = q
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A18;
thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A49
.= maxreal . ((minreal . (p9,q9)),q9) by A49
.= q by REAL_LAT:5 ; ::_thesis: verum
end;
A56: now__::_thesis:_for_p,_q,_r_being_Element_of_L9_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of L9; ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A18;
thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A49
.= minreal . (p,(minreal . (q,r))) by A49
.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4
.= minreal . ((p "/\" q),r) by A49
.= (p "/\" q) "/\" r by A49 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_L9_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of L9; ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A18;
thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A49
.= maxreal . (p,(maxreal . (q,r))) by A49
.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3
.= maxreal . ((p "\/" q),r) by A49
.= (p "\/" q) "\/" r by A49 ; ::_thesis: verum
end;
then  ( L9 is join-commutative & L9 is join-associative & L9 is meet-absorbing & L9 is meet-commutative & L9 is meet-associative & L9 is join-absorbing ) by A52, A55, A54, A56, A53, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L9 = L9 as Lattice ;
reconsider L9 = L9 as SubLattice of RealSubLatt (0,1) by A13, A12, A11, A16, NAT_LAT:def_12;
take  L9 ; ::_thesis: ( L9 is \/-inheriting & not L9 is /\-inheriting )
now__::_thesis:_for_X_being_Subset_of_L9_holds_"\/"_(X,L)_in_the_carrier_of_L9
let X be Subset of L9; ::_thesis: "\/" (X,L) in the carrier of L9
thus  "\/" (X,L) in the carrier of L9 ::_thesis: verum
proof
 0 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
then reconsider w = 0 as Element of L by A13, RCOMP_1:def_1;
A57: X is_less_than "\/" (X,L) by LATTICE3:def_21;
 "\/" (X,L) in [.0,1.] by A13;
then  "\/" (X,L) in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider y being Element of REAL  such that
A58: y = "\/" (X,L) and
 0 <= y and
A59: y <= 1 ;
assume A60: not "\/" (X,L) in the carrier of L9 ; ::_thesis: contradiction
then  not "\/" (X,L) in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  by A9, XBOOLE_0:def_3;
then A61: y <= 1 / 2 by A58, A59;
now__::_thesis:_for_z9_being_set_st_z9_in_X_holds_
z9_in_{0}
let z9 be set ; ::_thesis: ( z9 in X implies z9 in {0} )
assume A62: z9 in X ; ::_thesis: z9 in {0}
then reconsider z = z9 as Element of L9 ;
reconsider z = z as Element of L by A13, A14;
A63: z [= "\/" (X,L) by A57, A62, LATTICE3:def_17;
reconsider z1 = z as Element of REAL by TARSKI:def_3;
min (z1,y) = minreal . (z,("\/" (X,L))) by A58, REAL_LAT:def_1
.= (minreal || A) . [z,("\/" (X,L))] by A13, FUNCT_1:49
.= (minreal || A) . (z,("\/" (X,L)))
.= z "/\" ("\/" (X,L)) by A11, LATTICES:def_2
.= z1 by A63, LATTICES:4 ;
then  z1 <= y by XXREAL_0:def_9;
then  y + z1 <= (1 / 2) + y by A61, XREAL_1:7;
then  for v being Element of REAL holds
( not z1 = v or not 1 / 2 < v or not v <= 1 ) by XREAL_1:6;
then  not z1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ;
hence  z9 in {0} by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
then A64: X c= {0} by TARSKI:def_3;
now__::_thesis:_contradiction
percases ( X = {} or X = {0} ) by A64, ZFMISC_1:33;
supposeA65: X = {} ; ::_thesis: contradiction
A66: now__::_thesis:_for_r1_being_Element_of_L_st_X_is_less_than_r1_holds_
w_[=_r1
let r1 be Element of L; ::_thesis: ( X is_less_than r1 implies w [= r1 )
assume  X is_less_than r1 ; ::_thesis: w [= r1
 r1 in [.0,1.] by A13;
then  r1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider e being Element of REAL  such that
A67: r1 = e and
A68: 0 <= e and
 e <= 1 ;
w "/\" r1 = (minreal || A) . (w,r1) by A11, LATTICES:def_2
.= minreal . [w,r1] by A13, FUNCT_1:49
.= minreal . (w,r1)
.= min (0,e) by A67, REAL_LAT:def_1
.= w by A68, XXREAL_0:def_9 ;
hence  w [= r1 by LATTICES:4; ::_thesis: verum
end;
 for q being Element of L st q in X holds
q [= w by A65;
then  X is_less_than w by LATTICE3:def_17;
then  "\/" (X,L) = w by A66, LATTICE3:def_21;
then  "\/" (X,L) in {0} by TARSKI:def_1;
hence  contradiction by A9, A60, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose X = {0} ; ::_thesis: contradiction
then  "\/" (X,L) = w by LATTICE3:42;
then  "\/" (X,L) in {0} by TARSKI:def_1;
hence  contradiction by A9, A60, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
hence  L9 is \/-inheriting by Def3; ::_thesis: not L9 is /\-inheriting
now__::_thesis:_not_for_X_being_Subset_of_L9_holds_"/\"_(X,L)_in_the_carrier_of_L9
 1 / 2 in  {  x where x is Element of REAL : ( 0 <= x & x <= 1 )  }  ;
then reconsider z = 1 / 2 as Element of L by A13, RCOMP_1:def_1;
set X =  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ;
 for y being Element of REAL holds
( not y = 1 / 2 or not 1 / 2 < y or not y <= 1 ) ;
then A69: ( not 1 / 2 in {0} & not 1 / 2 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  ) by TARSKI:def_1;
 for x1 being set st x1 in  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  holds
x1 in B by A9, XBOOLE_0:def_3;
then reconsider X =  {  x where x is Element of REAL : ( 1 / 2 < x & x <= 1 )  }  as Subset of L9 by TARSKI:def_3;
take X = X; ::_thesis: not "/\" (X,L) in the carrier of L9
A70: now__::_thesis:_for_b_being_Element_of_L_st_b_is_less_than_X_holds_
b_[=_z
let b be Element of L; ::_thesis: ( b is_less_than X implies b [= z )
 b in A by A13;
then  b in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider b9 being Element of REAL  such that
A71: b = b9 and
A72: 0 <= b9 and
A73: b9 <= 1 ;
assume A74: b is_less_than X ; ::_thesis: b [= z
A75: b9 <= 1 / 2
proof
assume A76: 1 / 2 < b9 ; ::_thesis: contradiction
then  b9 in X by A73;
then A77: b = "/\" (X,L) by A71, A74, LATTICE3:41;
 (1 / 2) + b9 < b9 + b9 by A76, XREAL_1:6;
then A78: ((1 / 2) + b9) / 2 < (b9 + b9) / 2 by XREAL_1:74;
then  (((1 / 2) + b9) / 2) + b9 <= b9 + 1 by A73, XREAL_1:7;
then A79: ((1 / 2) + b9) / 2 <= 1 by XREAL_1:6;
then  ((1 / 2) + b9) / 2 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by A72;
then reconsider c = ((1 / 2) + b9) / 2 as Element of L by A13, RCOMP_1:def_1;
 (1 / 2) + (1 / 2) < b9 + (1 / 2) by A76, XREAL_1:6;
then  1 / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;
then  ((1 / 2) + b9) / 2 in X by A79;
then  b [= c by A77, LATTICE3:38;
then b9 = b "/\" c by A71, LATTICES:4
.= (minreal || A) . (b,c) by A11, LATTICES:def_2
.= minreal . [b,c] by A13, FUNCT_1:49
.= minreal . (b,c)
.= min (b9,(((1 / 2) + b9) / 2)) by A71, REAL_LAT:def_1 ;
hence  contradiction by A78, XXREAL_0:def_9; ::_thesis: verum
end;
b "/\" z = (minreal || A) . (b,z) by A11, LATTICES:def_2
.= minreal . [b,z] by A13, FUNCT_1:49
.= minreal . (b,z)
.= min (b9,(1 / 2)) by A71, REAL_LAT:def_1
.= b by A71, A75, XXREAL_0:def_9 ;
hence  b [= z by LATTICES:4; ::_thesis: verum
end;
now__::_thesis:_for_q_being_Element_of_L_st_q_in_X_holds_
z_[=_q
let q be Element of L; ::_thesis: ( q in X implies z [= q )
assume  q in X ; ::_thesis: z [= q
then A80: ex y being Element of REAL st
( q = y & 1 / 2 < y & y <= 1 ) ;
 q in A by A13;
then  q in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider q9 being Element of REAL  such that
A81: q = q9 and
 0 <= q9 and
 q9 <= 1 ;
z "/\" q = (minreal || A) . (z,q) by A11, LATTICES:def_2
.= minreal . [z,q] by A13, FUNCT_1:49
.= minreal . (z,q)
.= min ((1 / 2),q9) by A81, REAL_LAT:def_1
.= z by A81, A80, XXREAL_0:def_9 ;
hence  z [= q by LATTICES:4; ::_thesis: verum
end;
then  z is_less_than X by LATTICE3:def_16;
then  "/\" (X,L) = 1 / 2 by A70, LATTICE3:34;
hence  not "/\" (X,L) in the carrier of L9 by A1, A69, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  not L9 is /\-inheriting by Def2; ::_thesis: verum
end;

theorem :: MSUALG_7:22
ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting )
proof
reconsider L = RealSubLatt (0,1) as complete Lattice by Th20;
take  L ; ::_thesis: ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting )
thus  ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting ) by Th21; ::_thesis: verum
end;

theorem Th23: :: MSUALG_7:23
ex L9 being SubLattice of RealSubLatt (0,1) st
( L9 is /\-inheriting & not L9 is \/-inheriting )
proof
set B = {0,1} \/ ].0,(1 / 2).[;
set L = RealSubLatt (0,1);
set R = Real_Lattice ;
A1: {0,1} \/ ].0,(1 / 2).[ c= {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {0,1} \/ ].0,(1 / 2).[ or x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  )
assume A2: x1 in {0,1} \/ ].0,(1 / 2).[ ; ::_thesis: x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }
now__::_thesis:_x1_in_{1}_\/__{__x_where_x_is_Element_of_REAL_:_(_0_<=_x_&_x_<_1_/_2_)__}_
percases ( x1 in {0,1} or x1 in ].0,(1 / 2).[ ) by A2, XBOOLE_0:def_3;
suppose x1 in {0,1} ; ::_thesis: x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }
then  ( x1 = 0 or x1 = 1 ) by TARSKI:def_2;
then  ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by TARSKI:def_1;
hence  x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x1 in ].0,(1 / 2).[ ; ::_thesis: x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }
then  x1 in  {  r where r is Real : ( 0 < r & r < 1 / 2 )  }  by RCOMP_1:def_2;
then consider y being Element of REAL  such that
A3: x1 = y and
A4: ( 0 < y & y < 1 / 2 ) ;
 y in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A4;
hence  x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: verum
end;
 {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  c= {0,1} \/ ].0,(1 / 2).[
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  or x1 in {0,1} \/ ].0,(1 / 2).[ )
assume A5: x1 in {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: x1 in {0,1} \/ ].0,(1 / 2).[
now__::_thesis:_x1_in_{0,1}_\/_].0,(1_/_2).[
percases ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A5, XBOOLE_0:def_3;
suppose x1 in {1} ; ::_thesis: x1 in {0,1} \/ ].0,(1 / 2).[
then  x1 = 1 by TARSKI:def_1;
then  x1 in {0,1} by TARSKI:def_2;
hence  x1 in {0,1} \/ ].0,(1 / 2).[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: x1 in {0,1} \/ ].0,(1 / 2).[
then consider y being Element of REAL  such that
A6: x1 = y and
A7: ( 0 <= y & y < 1 / 2 ) ;
 ( y in  {  r where r is Real : ( 0 < r & r < 1 / 2 )  }  or y = 0 ) by A7;
then  ( y in ].0,(1 / 2).[ or y in {0,1} ) by RCOMP_1:def_2, TARSKI:def_2;
hence  x1 in {0,1} \/ ].0,(1 / 2).[ by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x1 in {0,1} \/ ].0,(1 / 2).[ ; ::_thesis: verum
end;
then A8: {0,1} \/ ].0,(1 / 2).[ = {1} \/  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A1, XBOOLE_0:def_10;
A9: 1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
then reconsider A = [.0,1.] as non empty set by RCOMP_1:def_1;
A10: now__::_thesis:_for_x1_being_Element_of_A_holds_x1_is_Element_of_Real_Lattice
let x1 be Element of A; ::_thesis: x1 is Element of Real_Lattice
 x1 in A ;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then  ex y1 being Element of REAL st
( x1 = y1 & 0 <= y1 & y1 <= 1 ) ;
hence  x1 is Element of Real_Lattice by REAL_LAT:def_3; ::_thesis: verum
end;
reconsider B = {0,1} \/ ].0,(1 / 2).[ as non empty set ;
A11: the L_meet of (RealSubLatt (0,1)) = minreal || [.0,1.] by Def4;
set Ma = maxreal || A;
set Mi = minreal || A;
A12: the L_join of (RealSubLatt (0,1)) = maxreal || [.0,1.] by Def4;
A13: A = the carrier of (RealSubLatt (0,1)) by Def4;
then reconsider Ma = maxreal || A, Mi = minreal || A as BinOp of A by Def4;
A14: now__::_thesis:_for_x1_being_set_st_x1_in_B_holds_
x1_in_A
let x1 be set ; ::_thesis: ( x1 in B implies x1 in A )
assume A15: x1 in B ; ::_thesis: x1 in A
now__::_thesis:_x1_in_A
percases ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A15, XBOOLE_0:def_3;
suppose x1 in {1} ; ::_thesis: x1 in A
then  x1 = 1 by TARSKI:def_1;
hence  x1 in A by A9, RCOMP_1:def_1; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: x1 in A
then consider y being Element of REAL  such that
A16: ( x1 = y & 0 <= y ) and
A17: y < 1 / 2 ;
 y + (1 / 2) <= (1 / 2) + 1 by A17, XREAL_1:7;
then  y <= 1 by XREAL_1:6;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by A16;
hence  x1 in A by RCOMP_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x1 in A ; ::_thesis: verum
end;
then A18: B c= A by TARSKI:def_3;
then A19: [:B,B:] c= [:A,A:] by ZFMISC_1:96;
then reconsider ma = Ma || B, mi = Mi || B as Function of [:B,B:],A by FUNCT_2:32;
A20: dom ma = [:B,B:] by FUNCT_2:def_1;
A21: now__::_thesis:_for_x9_being_set_st_x9_in_dom_ma_holds_
ma_._x9_in_B
let x9 be set ; ::_thesis: ( x9 in dom ma implies ma . x9 in B )
assume A22: x9 in dom ma ; ::_thesis: ma . x9 in B
then consider x1, x2 being set  such that
A23: x9 = [x1,x2] by RELAT_1:def_1;
A24: x2 in B by A22, A23, ZFMISC_1:87;
A25: x1 in B by A22, A23, ZFMISC_1:87;
now__::_thesis:_ma_._x9_in_B
percases ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A25, XBOOLE_0:def_3;
suppose x1 in {1} ; ::_thesis: ma . x9 in B
then A26: x1 = 1 by TARSKI:def_1;
now__::_thesis:_ma_._x9_in_B
percases ( x2 in {1} or x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A24, XBOOLE_0:def_3;
suppose x2 in {1} ; ::_thesis: ma . x9 in B
then A27: x2 = 1 by TARSKI:def_1;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (1,1) by A26, A27, REAL_LAT:def_2
.= 1 ;
then  ma . x9 in {1} by TARSKI:def_1;
hence  ma . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: ma . x9 in B
then consider y2 being Element of REAL  such that
A28: x2 = y2 and
A29: ( 0 <= y2 & y2 < 1 / 2 ) ;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (1,y2) by A26, A28, REAL_LAT:def_2 ;
then  ( ma . x9 = 1 or ma . x9 = y2 ) by XXREAL_0:16;
then  ( ma . x9 in {1} or ma . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A29, TARSKI:def_1;
hence  ma . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: ma . x9 in B
then consider y1 being Element of REAL  such that
A30: x1 = y1 and
A31: ( 0 <= y1 & y1 < 1 / 2 ) ;
now__::_thesis:_ma_._x9_in_B
percases ( x2 in {1} or x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A24, XBOOLE_0:def_3;
suppose x2 in {1} ; ::_thesis: ma . x9 in B
then A32: x2 = 1 by TARSKI:def_1;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (y1,1) by A30, A32, REAL_LAT:def_2 ;
then  ( ma . x9 = y1 or ma . x9 = 1 ) by XXREAL_0:16;
then  ( ma . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  or ma . x9 in {1} ) by A31, TARSKI:def_1;
hence  ma . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: ma . x9 in B
then consider y2 being Element of REAL  such that
A33: x2 = y2 and
A34: ( 0 <= y2 & y2 < 1 / 2 ) ;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (y1,y2) by A30, A33, REAL_LAT:def_2 ;
then  ( ma . x9 = y1 or ma . x9 = y2 ) by XXREAL_0:16;
then  ma . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A31, A34;
hence  ma . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
end;
end;
hence  ma . x9 in B ; ::_thesis: verum
end;
A35: dom mi = [:B,B:] by FUNCT_2:def_1;
A36: now__::_thesis:_for_x9_being_set_st_x9_in_dom_mi_holds_
mi_._x9_in_B
let x9 be set ; ::_thesis: ( x9 in dom mi implies mi . x9 in B )
assume A37: x9 in dom mi ; ::_thesis: mi . x9 in B
then consider x1, x2 being set  such that
A38: x9 = [x1,x2] by RELAT_1:def_1;
A39: x2 in B by A37, A38, ZFMISC_1:87;
A40: x1 in B by A37, A38, ZFMISC_1:87;
now__::_thesis:_mi_._x9_in_B
percases ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A40, XBOOLE_0:def_3;
suppose x1 in {1} ; ::_thesis: mi . x9 in B
then A41: x1 = 1 by TARSKI:def_1;
now__::_thesis:_mi_._x9_in_B
percases ( x2 in {1} or x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A39, XBOOLE_0:def_3;
suppose x2 in {1} ; ::_thesis: mi . x9 in B
then A42: x2 = 1 by TARSKI:def_1;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (1,1) by A41, A42, REAL_LAT:def_1
.= 1 ;
then  mi . x9 in {1} by TARSKI:def_1;
hence  mi . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: mi . x9 in B
then consider y2 being Element of REAL  such that
A43: x2 = y2 and
A44: ( 0 <= y2 & y2 < 1 / 2 ) ;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (1,y2) by A41, A43, REAL_LAT:def_1 ;
then  ( mi . x9 = 1 or mi . x9 = y2 ) by XXREAL_0:15;
then  ( mi . x9 in {1} or mi . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A44, TARSKI:def_1;
hence  mi . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: mi . x9 in B
then consider y1 being Element of REAL  such that
A45: x1 = y1 and
A46: ( 0 <= y1 & y1 < 1 / 2 ) ;
now__::_thesis:_mi_._x9_in_B
percases ( x2 in {1} or x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A1, A39, XBOOLE_0:def_3;
suppose x2 in {1} ; ::_thesis: mi . x9 in B
then A47: x2 = 1 by TARSKI:def_1;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (y1,1) by A45, A47, REAL_LAT:def_1 ;
then  ( mi . x9 = y1 or mi . x9 = 1 ) by XXREAL_0:15;
then  ( mi . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  or mi . x9 in {1} ) by A46, TARSKI:def_1;
hence  mi . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: mi . x9 in B
then consider y2 being Element of REAL  such that
A48: x2 = y2 and
A49: ( 0 <= y2 & y2 < 1 / 2 ) ;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (y1,y2) by A45, A48, REAL_LAT:def_1 ;
then  ( mi . x9 = y1 or mi . x9 = y2 ) by XXREAL_0:15;
then  mi . x9 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A46, A49;
hence  mi . x9 in B by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
end;
end;
hence  mi . x9 in B ; ::_thesis: verum
end;
reconsider L = RealSubLatt (0,1) as complete Lattice by Th20;
reconsider mi = mi as BinOp of B by A35, A36, FUNCT_2:3;
reconsider ma = ma as BinOp of B by A20, A21, FUNCT_2:3;
reconsider L9 = LattStr(# B,ma,mi #) as non empty LattStr ;
A50: now__::_thesis:_for_a,_b_being_Element_of_L9_holds_
(_a_"\/"_b_=_maxreal_._(a,b)_&_a_"/\"_b_=_minreal_._(a,b)_)
let a, b be Element of L9; ::_thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
A51: [a,b] in [:B,B:] ;
thus a "\/" b = the L_join of L9 . (a,b) by LATTICES:def_1
.= (maxreal || A) . [a,b] by FUNCT_1:49
.= maxreal . (a,b) by A19, A51, FUNCT_1:49 ; ::_thesis: a "/\" b = minreal . (a,b)
thus a "/\" b = the L_meet of L9 . (a,b) by LATTICES:def_2
.= (minreal || A) . [a,b] by FUNCT_1:49
.= minreal . (a,b) by A19, A51, FUNCT_1:49 ; ::_thesis: verum
end;
A52: now__::_thesis:_for_x1_being_Element_of_B_holds_x1_is_Element_of_L
let x1 be Element of B; ::_thesis: b1 is Element of L
percases ( x1 in {1} or x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by A8, XBOOLE_0:def_3;
suppose x1 in {1} ; ::_thesis: b1 is Element of L
then  x1 = 1 by TARSKI:def_1;
hence  x1 is Element of L by A9, A13, RCOMP_1:def_1; ::_thesis: verum
end;
suppose x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ; ::_thesis: b1 is Element of L
then consider y being Element of REAL  such that
A53: ( x1 = y & 0 <= y ) and
A54: y < 1 / 2 ;
 y + (1 / 2) <= (1 / 2) + 1 by A54, XREAL_1:7;
then  y <= 1 by XREAL_1:6;
then  x1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by A53;
hence  x1 is Element of L by A13, RCOMP_1:def_1; ::_thesis: verum
end;
end;
end;
A55: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of L9; ::_thesis: p "\/" q = q "\/" p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "\/" q = maxreal . (p,q) by A50
.= maxreal . (q9,p9) by REAL_LAT:1
.= q "\/" p by A50 ; ::_thesis: verum
end;
A56: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of L9; ::_thesis: p "/\" (p "\/" q) = p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A50
.= minreal . (p9,(maxreal . (p9,q9))) by A50
.= p by REAL_LAT:6 ; ::_thesis: verum
end;
A57: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of L9; ::_thesis: p "/\" q = q "/\" p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "/\" q = minreal . (p,q) by A50
.= minreal . (q9,p9) by REAL_LAT:2
.= q "/\" p by A50 ; ::_thesis: verum
end;
A58: now__::_thesis:_for_p,_q_being_Element_of_L9_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of L9; ::_thesis: (p "/\" q) "\/" q = q
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A50
.= maxreal . ((minreal . (p9,q9)),q9) by A50
.= q by REAL_LAT:5 ; ::_thesis: verum
end;
A59: now__::_thesis:_for_p,_q,_r_being_Element_of_L9_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of L9; ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A52;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A10;
thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A50
.= minreal . (p,(minreal . (q,r))) by A50
.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4
.= minreal . ((p "/\" q),r) by A50
.= (p "/\" q) "/\" r by A50 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_L9_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of L9; ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A52;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A10;
thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A50
.= maxreal . (p,(maxreal . (q,r))) by A50
.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3
.= maxreal . ((p "\/" q),r) by A50
.= (p "\/" q) "\/" r by A50 ; ::_thesis: verum
end;
then  ( L9 is join-commutative & L9 is join-associative & L9 is meet-absorbing & L9 is meet-commutative & L9 is meet-associative & L9 is join-absorbing ) by A55, A58, A57, A59, A56, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L9 = L9 as Lattice ;
reconsider L9 = L9 as SubLattice of RealSubLatt (0,1) by A13, A12, A11, A18, NAT_LAT:def_12;
take  L9 ; ::_thesis: ( L9 is /\-inheriting & not L9 is \/-inheriting )
now__::_thesis:_for_X_being_Subset_of_L9_holds_"/\"_(X,L)_in_the_carrier_of_L9
let X be Subset of L9; ::_thesis: "/\" (X,L) in the carrier of L9
thus  "/\" (X,L) in the carrier of L9 ::_thesis: verum
proof
 1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  ;
then reconsider w = 1 as Element of L by A13, RCOMP_1:def_1;
A60: "/\" (X,L) is_less_than X by LATTICE3:34;
 "/\" (X,L) in [.0,1.] by A13;
then  "/\" (X,L) in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider y being Element of REAL  such that
A61: y = "/\" (X,L) and
A62: 0 <= y and
 y <= 1 ;
assume A63: not "/\" (X,L) in the carrier of L9 ; ::_thesis: contradiction
then  not "/\" (X,L) in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  by A8, XBOOLE_0:def_3;
then A64: 1 / 2 <= y by A61, A62;
now__::_thesis:_for_z9_being_set_st_z9_in_X_holds_
z9_in_{1}
let z9 be set ; ::_thesis: ( z9 in X implies z9 in {1} )
assume A65: z9 in X ; ::_thesis: z9 in {1}
then reconsider z = z9 as Element of L9 ;
reconsider z = z as Element of L by A13, A14;
A66: "/\" (X,L) [= z by A60, A65, LATTICE3:def_16;
reconsider z1 = z as Element of REAL by TARSKI:def_3;
min (z1,y) = minreal . (z,("/\" (X,L))) by A61, REAL_LAT:def_1
.= (minreal || A) . [z,("/\" (X,L))] by A13, FUNCT_1:49
.= (minreal || A) . (z,("/\" (X,L)))
.= z "/\" ("/\" (X,L)) by A11, LATTICES:def_2
.= y by A61, A66, LATTICES:4 ;
then  y <= z1 by XXREAL_0:def_9;
then  y + (1 / 2) <= z1 + y by A64, XREAL_1:7;
then  for v being Element of REAL holds
( not z1 = v or not 0 <= v or not v < 1 / 2 ) by XREAL_1:6;
then  not z1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ;
hence  z9 in {1} by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
then A67: X c= {1} by TARSKI:def_3;
now__::_thesis:_contradiction
percases ( X = {} or X = {1} ) by A67, ZFMISC_1:33;
supposeA68: X = {} ; ::_thesis: contradiction
A69: now__::_thesis:_for_r1_being_Element_of_L_st_r1_is_less_than_X_holds_
r1_[=_w
let r1 be Element of L; ::_thesis: ( r1 is_less_than X implies r1 [= w )
assume  r1 is_less_than X ; ::_thesis: r1 [= w
 r1 in [.0,1.] by A13;
then  r1 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider e being Element of REAL  such that
A70: r1 = e and
 0 <= e and
A71: e <= 1 ;
r1 "/\" w = (minreal || A) . (r1,w) by A11, LATTICES:def_2
.= minreal . [r1,w] by A13, FUNCT_1:49
.= minreal . (r1,w)
.= min (e,1) by A70, REAL_LAT:def_1
.= r1 by A70, A71, XXREAL_0:def_9 ;
hence  r1 [= w by LATTICES:4; ::_thesis: verum
end;
 for q being Element of L st q in X holds
w [= q by A68;
then  w is_less_than X by LATTICE3:def_16;
then  "/\" (X,L) = w by A69, LATTICE3:34;
then  "/\" (X,L) in {1} by TARSKI:def_1;
hence  contradiction by A8, A63, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose X = {1} ; ::_thesis: contradiction
then  "/\" (X,L) = w by LATTICE3:42;
then  "/\" (X,L) in {1} by TARSKI:def_1;
hence  contradiction by A8, A63, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
hence  L9 is /\-inheriting by Def2; ::_thesis: not L9 is \/-inheriting
now__::_thesis:_not_for_X_being_Subset_of_L9_holds_"\/"_(X,L)_in_the_carrier_of_L9
 1 / 2 in  {  x where x is Element of REAL : ( 0 <= x & x <= 1 )  }  ;
then reconsider z = 1 / 2 as Element of L by A13, RCOMP_1:def_1;
set X =  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ;
 for y being Element of REAL holds
( not y = 1 / 2 or not 0 <= y or not y < 1 / 2 ) ;
then A72: ( not 1 / 2 in {1} & not 1 / 2 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  ) by TARSKI:def_1;
 for x1 being set st x1 in  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  holds
x1 in B by A8, XBOOLE_0:def_3;
then reconsider X =  {  x where x is Element of REAL : ( 0 <= x & x < 1 / 2 )  }  as Subset of L9 by TARSKI:def_3;
take X = X; ::_thesis: not "\/" (X,L) in the carrier of L9
A73: now__::_thesis:_for_b_being_Element_of_L_st_X_is_less_than_b_holds_
z_[=_b
let b be Element of L; ::_thesis: ( X is_less_than b implies z [= b )
 b in A by A13;
then  b in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider b9 being Element of REAL  such that
A74: b = b9 and
A75: 0 <= b9 and
A76: b9 <= 1 ;
assume A77: X is_less_than b ; ::_thesis: z [= b
A78: 1 / 2 <= b9
proof
 (1 / 2) + b9 <= 1 + 1 by A76, XREAL_1:7;
then  ((1 / 2) + b9) / 2 <= (1 + 1) / 2 by XREAL_1:72;
then  ((1 / 2) + b9) / 2 in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by A75;
then reconsider c = ((1 / 2) + b9) / 2 as Element of L by A13, RCOMP_1:def_1;
assume A79: b9 < 1 / 2 ; ::_thesis: contradiction
then  b9 + b9 < (1 / 2) + b9 by XREAL_1:6;
then A80: (b9 + b9) / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;
 b9 + (1 / 2) < (1 / 2) + (1 / 2) by A79, XREAL_1:6;
then  ((1 / 2) + b9) / 2 < 1 / 2 by XREAL_1:74;
then A81: ((1 / 2) + b9) / 2 in X by A75;
 b9 in X by A75, A79;
then  b = "\/" (X,L) by A74, A77, LATTICE3:40;
then  c [= b by A81, LATTICE3:38;
then ((1 / 2) + b9) / 2 = c "/\" b by LATTICES:4
.= (minreal || A) . (c,b) by A11, LATTICES:def_2
.= minreal . [c,b] by A13, FUNCT_1:49
.= minreal . (c,b)
.= min ((((1 / 2) + b9) / 2),b9) by A74, REAL_LAT:def_1 ;
hence  contradiction by A80, XXREAL_0:def_9; ::_thesis: verum
end;
z "/\" b = (minreal || A) . (z,b) by A11, LATTICES:def_2
.= minreal . [z,b] by A13, FUNCT_1:49
.= minreal . (z,b)
.= min ((1 / 2),b9) by A74, REAL_LAT:def_1
.= z by A78, XXREAL_0:def_9 ;
hence  z [= b by LATTICES:4; ::_thesis: verum
end;
now__::_thesis:_for_q_being_Element_of_L_st_q_in_X_holds_
q_[=_z
let q be Element of L; ::_thesis: ( q in X implies q [= z )
assume  q in X ; ::_thesis: q [= z
then A82: ex y being Element of REAL st
( q = y & 0 <= y & y < 1 / 2 ) ;
 q in A by A13;
then  q in  {  r where r is Real : ( 0 <= r & r <= 1 )  }  by RCOMP_1:def_1;
then consider q9 being Element of REAL  such that
A83: q = q9 and
 0 <= q9 and
 q9 <= 1 ;
q "/\" z = (minreal || A) . (q,z) by A11, LATTICES:def_2
.= minreal . [q,z] by A13, FUNCT_1:49
.= minreal . (q,z)
.= min (q9,(1 / 2)) by A83, REAL_LAT:def_1
.= q by A83, A82, XXREAL_0:def_9 ;
hence  q [= z by LATTICES:4; ::_thesis: verum
end;
then  X is_less_than z by LATTICE3:def_17;
then  "\/" (X,L) = 1 / 2 by A73, LATTICE3:def_21;
hence  not "\/" (X,L) in the carrier of L9 by A1, A72, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  not L9 is \/-inheriting by Def3; ::_thesis: verum
end;

theorem :: MSUALG_7:24
ex L being complete Lattice ex L9 being SubLattice of L st
( L9 is /\-inheriting & not L9 is \/-inheriting )
proof
reconsider L = RealSubLatt (0,1) as complete Lattice by Th20;
take  L ; ::_thesis: ex L9 being SubLattice of L st
( L9 is /\-inheriting & not L9 is \/-inheriting )
thus  ex L9 being SubLattice of L st
( L9 is /\-inheriting & not L9 is \/-inheriting ) by Th23; ::_thesis: verum
end;