let X be non empty Subset of VarPoset ; :: thesis: ( ex_sup_of X, VarPoset & sup X = meet X )
consider a being Element of X;
( meet X c= a & a is finite Subset of Vars ) by Th21, SETFAM_1:4;
then A1: ( meet X is finite & meet X c= Vars ) by XBOOLE_1:1;
for a being Element of X holds varcl a = a by Th21;
then varcl (meet X) = meet X by Th8;
then reconsider m = meet X as Element of VarPoset by A1, Th21;

A4: now

thus X is_<=_than m :: thesis: for b being Element of VarPoset st X is_<=_than b holds
m <= b

proof

let n be Element of VarPoset ; :: according to LATTICE3:def 9 :: thesis: ( not n in X or n <= m )
assume n in X ; :: thesis: n <= m
then m c= n by SETFAM_1:4;
hence n <= m by Th22; :: thesis: verum

end;

let b be Element of VarPoset ; :: thesis: ( X is_<=_than b implies m <= b )
assume A2: X is_<=_than b ; :: thesis: m <= b

now

let Y be set ; :: thesis: ( Y in X implies b c= Y )
assume A3: Y in X ; :: thesis: b c= Y
then reconsider c = Y as Element of VarPoset ;
c <= b by A2, A3, LATTICE3:def 9;
hence b c= Y by Th22; :: thesis: verum

end;

then b c= m by SETFAM_1:6;
hence m <= b by Th22; :: thesis: verum

end;

hence ex_sup_of X, VarPoset by YELLOW_0:15; :: thesis: sup X = meet X
hence sup X = meet X by A4, YELLOW_0:def 9; :: thesis: verum