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;

now

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

end;

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