let X, Y, 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 A1: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X ) ; :: thesis: ( not x in Y & not y in X & y in Y )
then A2: [:X,Y:] misses [:Y,X:] by ZFMISC_1:127;
A3: ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] implies ( not x in Y & not y in X & y in Y ) )
proof
assume ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] ) ; :: thesis: ( not x in Y & not y in X & y in Y )
then ( x in X & y in Y & ( not x in Y or not y in X ) ) by ZFMISC_1:106;
hence ( not x in Y & not y in X & y in Y ) by A1, XBOOLE_0:3; :: thesis: verum
end;
( [x,y] in [:Y,X:] implies [x,y] in [:X,Y:] )
proof
assume A4: ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; :: thesis: contradiction
not x in Y by A1, XBOOLE_0:3;
hence contradiction by A4, ZFMISC_1:106; :: thesis: verum
end;
hence ( not x in Y & not y in X & y in Y ) by A1, A2, A3, 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 A5: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y ) ; :: thesis: ( not y in X & not x in Y & x in X )
then A6: [:X,Y:] misses [:Y,X:] by ZFMISC_1:127;
A7: ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] implies ( not y in X & not x in Y & x in X ) )
proof
assume ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] ) ; :: thesis: ( not y in X & not x in Y & x in X )
then ( x in X & y in Y & ( not x in Y or not y in X ) ) by ZFMISC_1:106;
hence ( not y in X & not x in Y & x in X ) by A5, XBOOLE_0:3; :: thesis: verum
end;
( [x,y] in [:Y,X:] implies [x,y] in [:X,Y:] )
proof
assume A8: ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; :: thesis: contradiction
not y in X by A5, XBOOLE_0:3;
hence contradiction by A8, ZFMISC_1:106; :: thesis: verum
end;
hence ( not y in X & not x in Y & x in X ) by A5, A6, A7, XBOOLE_0:3, 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 A9: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y ) ; :: thesis: ( not x in X & not y in Y & y in X )
then A10: [:X,Y:] misses [:Y,X:] by ZFMISC_1:127;
A11: ( [x,y] in [:X,Y:] implies [x,y] in [:Y,X:] )
proof
assume A12: ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] ) ; :: thesis: contradiction
not x in X by A9, XBOOLE_0:3;
hence contradiction by A12, ZFMISC_1:106; :: 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:106;
hence ( not x in X & not y in Y & y in X ) by A9, XBOOLE_0:3; :: thesis: verum
end;
hence ( not x in X & not y in Y & y in X ) by A9, A10, A11, XBOOLE_0:3, XBOOLE_0:def 3; :: thesis: verum
end;
thus ( 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 ) ) :: thesis: verum
proof
assume A13: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X ) ; :: thesis: ( not x in X & not y in Y & x in Y )
then A14: [:X,Y:] misses [:Y,X:] by ZFMISC_1:127;
A15: ( [x,y] in [:X,Y:] implies [x,y] in [:Y,X:] )
proof
assume A16: ( [x,y] in [:X,Y:] & not [x,y] in [:Y,X:] ) ; :: thesis: contradiction
not y in Y by A13, XBOOLE_0:3;
hence contradiction by A16, ZFMISC_1:106; :: thesis: verum
end;
( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] implies ( not x in X & not y in Y & x in Y ) )
proof
assume ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; :: thesis: ( not x in X & not y in Y & x in Y )
then ( x in Y & y in X & ( not x in X or not y in Y ) ) by ZFMISC_1:106;
hence ( not x in X & not y in Y & x in Y ) by A13, XBOOLE_0:3; :: thesis: verum
end;
hence ( not x in X & not y in Y & x in Y ) by A13, A14, A15, XBOOLE_0:3, XBOOLE_0:def 3; :: thesis: verum
end;