let T be 1-sorted ; :: thesis: for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )
let A, B be Subset of T; :: thesis: ( A \/ B = [#] T iff A ` c= B )

hereby :: thesis: ( A ` c= B implies A \/ B = [#] T )

assume A \/ B = [#] T ; :: thesis: A ` c= B
then ([#] T) \ A = B \ A by XBOOLE_1:40;
hence A ` c= B by XBOOLE_1:36; :: thesis: verum

end;

assume A ` c= B ; :: thesis: A \/ B = [#] T
then A \/ (A `) c= A \/ B by XBOOLE_1:9;
then [#] T c= A \/ B by PRE_TOPC:2;
hence A \/ B = [#] T ; :: thesis: verum