let X, Y, Z be set ; :: thesis: ( Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) implies X c= Y )
assume Z <> {} ; :: thesis: ( ( not [:X,Z:] c= [:Y,Z:] & not [:Z,X:] c= [:Z,Y:] ) or X c= Y )
then consider z being object such that
A1: z in Z by XBOOLE_0:7;
assume A2: ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) ; :: thesis: X c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume x in X ; :: thesis: x in Y
then ( [x,z] in [:X,Z:] & [z,x] in [:Z,X:] ) by A1, Def2;
then ( [x,z] in [:Y,Z:] or [z,x] in [:Z,Y:] ) by A2;
hence x in Y by Lm16; :: thesis: verum