let U0 be strict with_const_op Universal_Algebra; :: thesis: UnSubAlLattice U0 is complete

let L be Subset of (UnSubAlLattice U0); :: according to VECTSP_8:def 6 :: thesis: ex b_{1} being Element of the carrier of (UnSubAlLattice U0) st

( b_{1} is_less_than L & ( for b_{2} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{2} is_less_than L or b_{2} [= b_{1} ) ) )

let L be Subset of (UnSubAlLattice U0); :: according to VECTSP_8:def 6 :: thesis: ex b

( b

( not b

per cases
( L = {} or L <> {} )
;

end;

suppose A1:
L = {}
; :: thesis: ex b_{1} being Element of the carrier of (UnSubAlLattice U0) st

( b_{1} is_less_than L & ( for b_{2} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{2} is_less_than L or b_{2} [= b_{1} ) ) )

( b

( not b

thus
ex b_{1} being Element of the carrier of (UnSubAlLattice U0) st

( b_{1} is_less_than L & ( for b_{2} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{2} is_less_than L or b_{2} [= b_{1} ) ) )
:: thesis: verum

end;( b

( not b

proof

take
Top (UnSubAlLattice U0)
; :: thesis: ( Top (UnSubAlLattice U0) is_less_than L & ( for b_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{1} is_less_than L or b_{1} [= Top (UnSubAlLattice U0) ) ) )

thus Top (UnSubAlLattice U0) is_less_than L by A1; :: thesis: for b_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{1} is_less_than L or b_{1} [= Top (UnSubAlLattice U0) )

let l2 be Element of (UnSubAlLattice U0); :: thesis: ( not l2 is_less_than L or l2 [= Top (UnSubAlLattice U0) )

assume l2 is_less_than L ; :: thesis: l2 [= Top (UnSubAlLattice U0)

thus l2 [= Top (UnSubAlLattice U0) by LATTICES:19; :: thesis: verum

end;( not b

thus Top (UnSubAlLattice U0) is_less_than L by A1; :: thesis: for b

( not b

let l2 be Element of (UnSubAlLattice U0); :: thesis: ( not l2 is_less_than L or l2 [= Top (UnSubAlLattice U0) )

assume l2 is_less_than L ; :: thesis: l2 [= Top (UnSubAlLattice U0)

thus l2 [= Top (UnSubAlLattice U0) by LATTICES:19; :: thesis: verum

suppose
L <> {}
; :: thesis: ex b_{1} being Element of the carrier of (UnSubAlLattice U0) st

( b_{1} is_less_than L & ( for b_{2} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{2} is_less_than L or b_{2} [= b_{1} ) ) )

( b

( not b

then reconsider H = L as non empty Subset of (Sub U0) ;

reconsider l1 = meet H as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;

take l1 ; :: thesis: ( l1 is_less_than L & ( for b_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{1} is_less_than L or b_{1} [= l1 ) ) )

set x = the Element of H;

thus l1 is_less_than L :: thesis: for b_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( not b_{1} is_less_than L or b_{1} [= l1 )

reconsider U1 = l3 as strict SubAlgebra of U0 by UNIALG_2:def 14;

assume A3: l3 is_less_than L ; :: thesis: l3 [= l1

A4: for A being set st A in (Carr U0) .: H holds

the carrier of U1 c= A

then the carrier of U1 c= meet ((Carr U0) .: H) by A4, SETFAM_1:5;

then the carrier of U1 c= the carrier of (meet H) by Def5;

hence l3 [= l1 by Th15; :: thesis: verum

end;reconsider l1 = meet H as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;

take l1 ; :: thesis: ( l1 is_less_than L & ( for b

( not b

set x = the Element of H;

thus l1 is_less_than L :: thesis: for b

( not b

proof

let l3 be Element of (UnSubAlLattice U0); :: thesis: ( not l3 is_less_than L or l3 [= l1 )
let l2 be Element of (UnSubAlLattice U0); :: according to LATTICE3:def 16 :: thesis: ( not l2 in L or l1 [= l2 )

reconsider U1 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;

reconsider u = l2 as Element of Sub U0 ;

assume A2: l2 in L ; :: thesis: l1 [= l2

(Carr U0) . u = the carrier of U1 by Def4;

then meet ((Carr U0) .: H) c= the carrier of U1 by A2, FUNCT_2:35, SETFAM_1:3;

then the carrier of (meet H) c= the carrier of U1 by Def5;

hence l1 [= l2 by Th15; :: thesis: verum

end;reconsider U1 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;

reconsider u = l2 as Element of Sub U0 ;

assume A2: l2 in L ; :: thesis: l1 [= l2

(Carr U0) . u = the carrier of U1 by Def4;

then meet ((Carr U0) .: H) c= the carrier of U1 by A2, FUNCT_2:35, SETFAM_1:3;

then the carrier of (meet H) c= the carrier of U1 by Def5;

hence l1 [= l2 by Th15; :: thesis: verum

reconsider U1 = l3 as strict SubAlgebra of U0 by UNIALG_2:def 14;

assume A3: l3 is_less_than L ; :: thesis: l3 [= l1

A4: for A being set st A in (Carr U0) .: H holds

the carrier of U1 c= A

proof

(Carr U0) . the Element of H in (Carr U0) .: L
by FUNCT_2:35;
let A be set ; :: thesis: ( A in (Carr U0) .: H implies the carrier of U1 c= A )

assume A5: A in (Carr U0) .: H ; :: thesis: the carrier of U1 c= A

then reconsider H1 = A as Subset of U0 ;

consider l4 being Element of Sub U0 such that

A6: ( l4 in H & H1 = (Carr U0) . l4 ) by A5, FUNCT_2:65;

reconsider l4 = l4 as Element of (UnSubAlLattice U0) ;

reconsider U2 = l4 as strict SubAlgebra of U0 by UNIALG_2:def 14;

( A = the carrier of U2 & l3 [= l4 ) by A3, A6, Def4;

hence the carrier of U1 c= A by Th15; :: thesis: verum

end;assume A5: A in (Carr U0) .: H ; :: thesis: the carrier of U1 c= A

then reconsider H1 = A as Subset of U0 ;

consider l4 being Element of Sub U0 such that

A6: ( l4 in H & H1 = (Carr U0) . l4 ) by A5, FUNCT_2:65;

reconsider l4 = l4 as Element of (UnSubAlLattice U0) ;

reconsider U2 = l4 as strict SubAlgebra of U0 by UNIALG_2:def 14;

( A = the carrier of U2 & l3 [= l4 ) by A3, A6, Def4;

hence the carrier of U1 c= A by Th15; :: thesis: verum

then the carrier of U1 c= meet ((Carr U0) .: H) by A4, SETFAM_1:5;

then the carrier of U1 c= the carrier of (meet H) by Def5;

hence l3 [= l1 by Th15; :: thesis: verum