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₁ being Element of the carrier of (UnSubAlLattice U0) st
( b₁ is_less_than L & ( for b₂ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₂ is_less_than L or b₂ [= b₁ ) ) )

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

suppose A1: L = {} ; :: thesis: ex b₁ being Element of the carrier of (UnSubAlLattice U0) st
( b₁ is_less_than L & ( for b₂ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₂ is_less_than L or b₂ [= b₁ ) ) )

thus ex b₁ being Element of the carrier of (UnSubAlLattice U0) st
( b₁ is_less_than L & ( for b₂ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₂ is_less_than L or b₂ [= b₁ ) ) ) :: thesis: verum

proof

take Top (UnSubAlLattice U0) ; :: thesis: ( Top (UnSubAlLattice U0) is_less_than L & ( for b₁ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₁ is_less_than L or b₁ [= Top (UnSubAlLattice U0) ) ) )
thus Top (UnSubAlLattice U0) is_less_than L by A1; :: thesis: for b₁ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₁ is_less_than L or b₁ [= 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;

end;

suppose L <> {} ; :: thesis: ex b₁ being Element of the carrier of (UnSubAlLattice U0) st
( b₁ is_less_than L & ( for b₂ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₂ is_less_than L or b₂ [= 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₁ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₁ is_less_than L or b₁ [= l1 ) ) )
set x = the Element of H;
thus l1 is_less_than L :: thesis: for b₁ being Element of the carrier of (UnSubAlLattice U0) holds
( not b₁ is_less_than L or b₁ [= l1 )

proof

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;

let l3 be Element of (UnSubAlLattice U0); :: thesis: ( not l3 is_less_than L or l3 [= 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

proof

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;

(Carr U0) . the Element of H in (Carr U0) .: L by FUNCT_2:35;
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;

end;