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 ; :: thesis: verum
end;
suppose B <> {} ; :: thesis: B c= D
then ( [:A,B:] <> {} & [:B,A:] <> {} ) by Th89;
hence B c= D by A1, Th113; :: thesis: verum
end;
end;