let A, B be non empty preBoolean set ; :: thesis: ( not A /\ B is empty & A /\ B is preBoolean )
( {} in A & {} in B ) by Th18;
then reconsider C = A /\ B as non empty set by XBOOLE_0:def 4;
C is preBoolean

proof

now

let X, Y be set ; :: thesis: ( X in C & Y in C implies ( X \/ Y in C & X \ Y in C ) )
assume ( X in C & Y in C ) ; :: thesis: ( X \/ Y in C & X \ Y in C )
then A1: ( X in A & Y in A & X in B & Y in B ) by XBOOLE_0:def 4;
then ( X \/ Y in A & X \/ Y in B ) by Th10;
hence X \/ Y in C by XBOOLE_0:def 4; :: thesis: X \ Y in C
( X \ Y in A & X \ Y in B ) by A1, Th10;
hence X \ Y in C by XBOOLE_0:def 4; :: thesis: verum

end;

hence C is preBoolean by Th10; :: thesis: verum

end;

hence ( not A /\ B is empty & A /\ B is preBoolean ) ; :: thesis: verum