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 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: ( [x,y] in [:Y,X:] implies [x,y] in [:X,Y:] )
proof
assume that
A5: [x,y] in [:Y,X:] and
not [x,y] in [:X,Y:] ; :: thesis: contradiction
not x in Y by A1, A3, XBOOLE_0:3;
hence contradiction by A5, ZFMISC_1:106; :: thesis: verum
end;
A6: ( [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 that
A7: [x,y] in [:X,Y:] and
not [x,y] in [:Y,X:] ; :: thesis: ( not x in Y & not y in X & y in Y )
( x in X & y in Y ) by A7, 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:] misses [:Y,X:] by A1, ZFMISC_1:127;
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
A8: X misses Y and
A9: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A10: y in Y ; :: thesis: ( not y in X & not x in Y & x in X )
A11: ( [x,y] in [:Y,X:] implies [x,y] in [:X,Y:] )
proof
assume that
A12: [x,y] in [:Y,X:] and
not [x,y] in [:X,Y:] ; :: thesis: contradiction
not y in X by A8, A10, XBOOLE_0:3;
hence contradiction by A12, ZFMISC_1:106; :: thesis: verum
end;
A13: ( [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 that
A14: [x,y] in [:X,Y:] and
not [x,y] in [:Y,X:] ; :: thesis: ( not y in X & not x in Y & x in X )
( x in X & y in Y ) by A14, ZFMISC_1:106;
hence ( not y in X & not x in Y & x in X ) by A8, XBOOLE_0:3; :: thesis: verum
end;
[:X,Y:] misses [:Y,X:] by A8, ZFMISC_1:127;
hence ( not y in X & not x in Y & x in X ) by A9, A13, 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 & 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
A15: X misses Y and
A16: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A17: x in Y ; :: thesis: ( not x in X & not y in Y & y in X )
A18: ( [x,y] in [:X,Y:] implies [x,y] in [:Y,X:] )
proof
assume that
A19: [x,y] in [:X,Y:] and
not [x,y] in [:Y,X:] ; :: thesis: contradiction
not x in X by A15, A17, XBOOLE_0:3;
hence contradiction by A19, ZFMISC_1:106; :: thesis: verum
end;
A20: ( [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 A15, XBOOLE_0:3; :: thesis: verum
end;
[:X,Y:] misses [:Y,X:] by A15, ZFMISC_1:127;
hence ( not x in X & not y in Y & y in X ) by A16, A18, A20, 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 that
A21: X misses Y and
A22: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A23: y in X ; :: thesis: ( not x in X & not y in Y & x in Y )
A24: ( [x,y] in [:X,Y:] implies [x,y] in [:Y,X:] )
proof
assume that
A25: [x,y] in [:X,Y:] and
not [x,y] in [:Y,X:] ; :: thesis: contradiction
not y in Y by A21, A23, XBOOLE_0:3;
hence contradiction by A25, ZFMISC_1:106; :: thesis: verum
end;
A26: ( [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 that
A27: [x,y] in [:Y,X:] and
not [x,y] in [:X,Y:] ; :: thesis: ( not x in X & not y in Y & x in Y )
( x in Y & y in X ) by A27, ZFMISC_1:106;
hence ( not x in X & not y in Y & x in Y ) by A21, XBOOLE_0:3; :: thesis: verum
end;
[:X,Y:] misses [:Y,X:] by A21, ZFMISC_1:127;
hence ( not x in X & not y in Y & x in Y ) by A22, A24, A26, XBOOLE_0:3, XBOOLE_0:def 3; :: thesis: verum
end;