let X, x be set ; :: thesis: ( x is Element of iff x c= X )
LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def 2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;
hence ( x is Element of implies x c= X ) ; :: thesis: ( x c= X implies x is Element of )
thus ( x c= X implies x is Element of ) by A1; :: thesis: verum