let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
let R be Subset of [:A,B:]; :: thesis: ( X <> {} implies R .:^ X c= R .: X )
assume A1: X <> {} ; :: thesis: R .:^ X c= R .: X
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in R .:^ X or y in R .: X )
assume A2: y in R .:^ X ; :: thesis: y in R .: X
consider x being set such that
A3: x in X by A1, XBOOLE_0:def 1;
y in Im R,x by A2, A3, Th24;
then [x,y] in R by Th9;
hence y in R .: X by A3, RELAT_1:def 13; :: thesis: verum