let A be set ; :: thesis: bool A is preBoolean

now

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 X' = X, Y' = Y as Subset of A ;
( X' \/ Y' in bool A & X' \ Y' in bool A ) ;
hence ( X \/ Y in bool A & X \ Y in bool A ) ; :: thesis: verum

end;

hence bool A is preBoolean by Th10; :: thesis: verum