let x, y be Element of ; :: thesis: ( x <= y iff y c= x )
set V = { (varcl A) where A is finite Subset of : verum } ;
consider A0 being finite Subset of ;
varcl A0 in { (varcl A) where A is finite Subset of : verum } ;
then reconsider V = { (varcl A) where A is finite Subset of : verum } as non empty set ;
reconsider a = x, b = y as Element of ;
( x <= y iff ~ a >= ~ b ) by YELLOW_7:1;
hence ( x <= y iff y c= x ) by YELLOW_1:3; :: thesis: verum