let U0 be strict with_const_op Universal_Algebra; :: thesis:
let L be Subset of (); :: according to VECTSP_8:def 6 :: thesis: ex b1 being Element of the carrier of () st
( b1 is_less_than L & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than L or b2 [= b1 ) ) )

per cases ( L = {} or L <> {} ) ;
suppose A1: L = {} ; :: thesis: ex b1 being Element of the carrier of () st
( b1 is_less_than L & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than L or b2 [= b1 ) ) )

thus ex b1 being Element of the carrier of () st
( b1 is_less_than L & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than L or b2 [= b1 ) ) ) :: thesis: verum
proof
take Top () ; :: thesis: ( Top () is_less_than L & ( for b1 being Element of the carrier of () holds
( not b1 is_less_than L or b1 [= Top () ) ) )

thus Top () is_less_than L by A1; :: thesis: for b1 being Element of the carrier of () holds
( not b1 is_less_than L or b1 [= Top () )

let l2 be Element of (); :: thesis: ( not l2 is_less_than L or l2 [= Top () )
assume l2 is_less_than L ; :: thesis: l2 [= Top ()
thus l2 [= Top () by LATTICES:19; :: thesis: verum
end;
end;
suppose L <> {} ; :: thesis: ex b1 being Element of the carrier of () st
( b1 is_less_than L & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than L or b2 [= b1 ) ) )

then reconsider H = L as non empty Subset of (Sub U0) ;
reconsider l1 = meet H as Element of () by UNIALG_2:def 14;
take l1 ; :: thesis: ( l1 is_less_than L & ( for b1 being Element of the carrier of () holds
( not b1 is_less_than L or b1 [= l1 ) ) )

set x = the Element of H;
thus l1 is_less_than L :: thesis: for b1 being Element of the carrier of () holds
( not b1 is_less_than L or b1 [= l1 )
proof
let l2 be Element of (); :: 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 ;
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 (); :: 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 ;
reconsider l4 = l4 as Element of () ;
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 ;
then the carrier of U1 c= the carrier of (meet H) by Def5;
hence l3 [= l1 by Th15; :: thesis: verum
end;
end;