set V = { (varcl A) where A is finite Subset of Vars : verum } ;
set A0 = the finite Subset of Vars;
varcl the finite Subset of Vars in { (varcl A) where A is finite Subset of Vars : verum } ;
then reconsider V = { (varcl A) where A is finite Subset of Vars : verum } as non empty set ;
now :: thesis: for x, y being set st x in V & y in V holds
x \/ y in V
let x, y be set ; :: thesis: ( x in V & y in V implies x \/ y in V )
assume x in V ; :: thesis: ( y in V implies x \/ y in V )
then consider A1 being finite Subset of Vars such that
A1: x = varcl A1 ;
assume y in V ; :: thesis: x \/ y in V
then consider A2 being finite Subset of Vars such that
A2: y = varcl A2 ;
x \/ y = varcl (A1 \/ A2) by A1, A2, Th11;
hence x \/ y in V ; :: thesis: verum
end;
then InclPoset V is with_suprema by YELLOW_1:11;
hence VarPoset is with_infima by LATTICE3:10; :: thesis: VarPoset is with_suprema
now :: thesis: for x, y being set st x in V & y in V holds
x /\ y in V
let x, y be set ; :: thesis: ( x in V & y in V implies x /\ y in V )
assume x in V ; :: thesis: ( y in V implies x /\ y in V )
then consider A1 being finite Subset of Vars such that
A3: x = varcl A1 ;
assume y in V ; :: thesis: x /\ y in V
then consider A2 being finite Subset of Vars such that
A4: y = varcl A2 ;
reconsider V1 = varcl A1, V2 = varcl A2 as finite Subset of Vars by Th24;
x /\ y = varcl (V1 /\ V2) by A3, A4, Th13;
hence x /\ y in V ; :: thesis: verum
end;
then InclPoset V is with_infima by YELLOW_1:12;
hence VarPoset is with_suprema by YELLOW_7:16; :: thesis: verum