let X be non empty Subset of VarPoset; :: thesis: ( ex_sup_of X, VarPoset & sup X = meet X )
set a = the Element of X;
A1: meet X c= the Element of X by SETFAM_1:3;
A2: the Element of X is finite Subset of Vars by Th110;
then A3: meet X c= Vars by A1, XBOOLE_1:1;
for a being Element of X holds varcl a = a by Th110;
then varcl (meet X) = meet X by Th12;
then reconsider m = meet X as Element of VarPoset by A1, A2, A3, Th110;
A4: now :: thesis: ( X is_<=_than m & ( for b being Element of VarPoset st X is_<=_than b holds
m <= b ) )
thus X is_<=_than m by SETFAM_1:3, Th109; :: thesis: for b being Element of VarPoset st X is_<=_than b holds
m <= b
let b be Element of VarPoset; :: thesis: ( X is_<=_than b implies m <= b )
assume A5: X is_<=_than b ; :: thesis: m <= b
for Y being set st Y in X holds
b c= Y by Th109, A5;
then b c= m by SETFAM_1:5;
hence m <= b by Th109; :: 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