let A be non empty set ; 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 ; ( ( [: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:] )
; B c= D