let x, y be object ; :: thesis: for X, Y being set
for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
let X, Y be set ; :: thesis: for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
let R be Relation; :: thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) :: thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof
assume that
A1: X misses Y and
A2: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A3: x in X ; :: thesis: ( not x in Y & not y in X & y in Y )
A4: not [x,y] in [:Y,X:]
proof
assume A5: [x,y] in [:Y,X:] ; :: thesis: contradiction
not x in Y by A1, A3, XBOOLE_0:3;
hence contradiction by A5, ZFMISC_1:87; :: thesis: verum
end;
A6: ( [x,y] in [:X,Y:] implies ( not x in Y & not y in X & y in Y ) )
proof
assume [x,y] in [:X,Y:] ; :: thesis: ( not x in Y & not y in X & y in Y )
then ( x in X & y in Y ) by ZFMISC_1:87;
hence ( not x in Y & not y in X & y in Y ) by A1, XBOOLE_0:3; :: thesis: verum
end;
[:X,Y:] misses [:Y,X:] by A1, ZFMISC_1:104;
hence ( not x in Y & not y in X & y in Y ) by A2, A6, A4, XBOOLE_0:5; :: thesis: verum
end;
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) :: thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof
assume that
A7: X misses Y and
A8: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A9: y in Y ; :: thesis: ( not y in X & not x in Y & x in X )
A10: not [x,y] in [:Y,X:]
proof
assume A11: [x,y] in [:Y,X:] ; :: thesis: contradiction
not y in X by A7, A9, XBOOLE_0:3;
hence contradiction by A11, ZFMISC_1:87; :: thesis: verum
end;
( [x,y] in [:X,Y:] implies ( not y in X & not x in Y & x in X ) )
proof
assume [x,y] in [:X,Y:] ; :: thesis: ( not y in X & not x in Y & x in X )
then ( x in X & y in Y ) by ZFMISC_1:87;
hence ( not y in X & not x in Y & x in X ) by A7, XBOOLE_0:3; :: thesis: verum
end;
hence ( not y in X & not x in Y & x in X ) by A8, A10, XBOOLE_0:def 3; :: thesis: verum
end;
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) :: thesis: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) )
proof
assume that
A12: X misses Y and
A13: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A14: x in Y ; :: thesis: ( not x in X & not y in Y & y in X )
A15: not [x,y] in [:X,Y:]
proof
assume A16: [x,y] in [:X,Y:] ; :: thesis: contradiction
not x in X by A12, A14, XBOOLE_0:3;
hence contradiction by A16, ZFMISC_1:87; :: thesis: verum
end;
( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] implies ( not x in X & not y in Y & y in X ) )
proof
assume ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; :: thesis: ( not x in X & not y in Y & y in X )
then ( ( x in Y & y in X & not x in X ) or ( x in Y & y in X & not y in Y ) ) by ZFMISC_1:87;
hence ( not x in X & not y in Y & y in X ) by A12, XBOOLE_0:3; :: thesis: verum
end;
hence ( not x in X & not y in Y & y in X ) by A13, A15, XBOOLE_0:def 3; :: thesis: verum
end;
assume that
A17: X misses Y and
A18: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A19: y in X ; :: thesis: ( not x in X & not y in Y & x in Y )
A20: not [x,y] in [:X,Y:]
proof
assume A21: [x,y] in [:X,Y:] ; :: thesis: contradiction
not y in Y by A17, A19, XBOOLE_0:3;
hence contradiction by A21, ZFMISC_1:87; :: thesis: verum
end;
( [x,y] in [:Y,X:] implies ( not x in X & not y in Y & x in Y ) )
proof
assume [x,y] in [:Y,X:] ; :: thesis: ( not x in X & not y in Y & x in Y )
then ( x in Y & y in X ) by ZFMISC_1:87;
hence ( not x in X & not y in Y & x in Y ) by A17, XBOOLE_0:3; :: thesis: verum
end;
hence ( not x in X & not y in Y & x in Y ) by A18, A20, XBOOLE_0:def 3; :: thesis: verum