let X, x be set ; :: thesis: ( x is Element of (BoolePoset X) 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 (BoolePoset X) implies x c= X ) ; :: thesis: ( x c= X implies x is Element of (BoolePoset X) )
thus ( x c= X implies x is Element of (BoolePoset X) ) by A1; :: thesis: verum