let X be set ; :: thesis: for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)
let R be Relation; :: thesis: (dom R) /\ X c= (R ~) .: (R .: X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R) /\ X or x in (R ~) .: (R .: X) )
assume A1: x in (dom R) /\ X ; :: thesis: x in (R ~) .: (R .: X)
then x in dom R by XBOOLE_0:def 4;
then consider y being set such that
A2: [x,y] in R by Def4;
A3: [y,x] in R ~ by A2, Def7;
x in X by A1, XBOOLE_0:def 4;
then y in R .: X by A2, Def13;
hence x in (R ~) .: (R .: X) by A3, Def13; :: thesis: verum