let A, B be set ; :: thesis: for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))
let R be Subset of [:A,B:]; :: thesis: for X being set holds R .: X = R .: (X /\ (proj1 R))
let X be set ; :: thesis: R .: X = R .: (X /\ (proj1 R))
thus R .: X c= R .: (X /\ (proj1 R)) :: according to XBOOLE_0:def 10 :: thesis: R .: (X /\ (proj1 R)) c= R .: X
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: X or y in R .: (X /\ (proj1 R)) )
assume y in R .: X ; :: thesis: y in R .: (X /\ (proj1 R))
then consider x being object such that
A1: [x,y] in R and
A2: x in X by RELAT_1:def 13;
x in proj1 R by A1, XTUPLE_0:def 12;
then x in X /\ (proj1 R) by A2, XBOOLE_0:def 4;
hence y in R .: (X /\ (proj1 R)) by A1, RELAT_1:def 13; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (X /\ (proj1 R)) or y in R .: X )
assume y in R .: (X /\ (proj1 R)) ; :: thesis: y in R .: X
then consider x being object such that
A3: [x,y] in R and
A4: x in X /\ (proj1 R) by RELAT_1:def 13;
x in X by A4, XBOOLE_0:def 4;
hence y in R .: X by A3, RELAT_1:def 13; :: thesis: verum