let A be set ; :: thesis: bool A is preBoolean
now :: thesis: for X, Y being set st X in bool A & Y in bool A holds
( X \/ Y in bool A & X \ Y in bool A )
let X, Y be set ; :: thesis: ( X in bool A & Y in bool A implies ( X \/ Y in bool A & X \ Y in bool A ) )
assume ( X in bool A & Y in bool A ) ; :: thesis: ( X \/ Y in bool A & X \ Y in bool A )
then reconsider X9 = X, Y9 = Y as Subset of A ;
( X9 \/ Y9 in bool A & X9 \ Y9 in bool A ) ;
hence ( X \/ Y in bool A & X \ Y in bool A ) ; :: thesis: verum
end;
hence bool A is preBoolean by Th1; :: thesis: verum