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

now :: thesis: for X, Y being set st X in C & Y in C holds
( X \/ Y in C & X \ Y in C )

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 Th1;
A4: X \ Y in B by A2, Th1;
A5: ( X in A & Y in A ) by A1, XBOOLE_0:def 4;
then X \/ Y in A by Th1;
hence X \/ Y in C by A3, XBOOLE_0:def 4; :: thesis: X \ Y in C
X \ Y in A by A5, Th1;
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 Th1; :: thesis: verum