let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}
let R be Subset of [:A,B:]; :: thesis: ( R = {} & X <> {} implies R .:^ X = {} )
assume that
A1: R = {} and
A2: X <> {} ; :: thesis: R .:^ X = {}
R .:^ X c= {}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in R .:^ X or a in {} )
assume A3: a in R .:^ X ; :: thesis: a in {}
consider x being object such that
A4: x in X by A2, XBOOLE_0:def 1;
a in Im (R,x) by A3, A4, Th24;
hence a in {} by A1; :: thesis: verum

end;

hence R .:^ X = {} ; :: thesis: verum