let A be non empty set ; :: thesis: for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds
B c= D
let B, C, D be set ; :: thesis: ( ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) implies B c= D )
assume A1: ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) ; :: thesis: B c= D

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: B c= D

hence B c= D by XBOOLE_1:2; :: thesis: verum

end;

suppose B <> {} ; :: thesis: B c= D

then ( [:A,B:] <> {} & [:B,A:] <> {} ) by Th113;
hence B c= D by A1, Th138; :: thesis: verum

end;

end;