let X be set ; :: thesis: for R being Relation st X c= dom R holds
X c= R " (R .: X)
let R be Relation; :: thesis: ( X c= dom R implies X c= R " (R .: X) )
assume A1: X c= dom R ; :: thesis: X c= R " (R .: X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in R " (R .: X) )
assume A2: x in X ; :: thesis: x in R " (R .: X)
then consider Rx being set such that
A3: [x,Rx] in R by A1, RELAT_1:def 4;
Rx in R .: X by A2, A3, RELAT_1:def 13;
hence x in R " (R .: X) by A3, RELAT_1:def 14; :: thesis: verum