let x, y be Element of VarPoset; :: thesis: ( x <= y iff y c= x )
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 ;
reconsider a = x, b = y as Element of ((InclPoset V) opp) ;
( x <= y iff ~ a >= ~ b ) by YELLOW_7:1;
hence ( x <= y iff y c= x ) by YELLOW_1:3; :: thesis: verum