let R be 1-sorted ; :: thesis: for X, Y being Subset of R holds
( X c= Y iff (X `) \/ Y = [#] R )
let X, Y be Subset of R; :: thesis: ( X c= Y iff (X `) \/ Y = [#] R )
thus ( X c= Y implies (X `) \/ Y = [#] R ) :: thesis: ( (X `) \/ Y = [#] R implies X c= Y )
proof
assume X c= Y ; :: thesis: (X `) \/ Y = [#] R
then X \ Y = {} by XBOOLE_1:37;
then (X \ Y) ` = [#] R ;
hence (X `) \/ Y = [#] R by SUBSET_1:14; :: thesis: verum
end;
assume (X `) \/ Y = [#] R ; :: thesis: X c= Y
then ((X \ Y) `) ` = (({} R) `) ` by SUBSET_1:14;
hence X c= Y by XBOOLE_1:37; :: thesis: verum