let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
let R be Subset of [:A,B:]; :: thesis: ( (.: R) .: {_{X}_} = {} iff X = {} )
thus ( (.: R) .: {_{X}_} = {} implies X = {} ) :: thesis: ( X = {} implies (.: R) .: {_{X}_} = {} )
proof
assume (.: R) .: {_{X}_} = {} ; :: thesis: X = {}
then dom (.: R) misses {_{X}_} by RELAT_1:118;
then A1: bool A misses {_{X}_} by Def1;
{_{X}_} c= bool A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} or y in bool A )
reconsider yy = y as set by TARSKI:1;
assume y in {_{X}_} ; :: thesis: y in bool A
then consider x being object such that
A2: y = {x} and
A3: x in X by Th1;
A4: x in A by A3;
yy c= A by A2, A4, TARSKI:def 1;
hence y in bool A ; :: thesis: verum
end;
then A5: (bool A) /\ {_{X}_} = {_{X}_} by XBOOLE_1:28;
assume X <> {} ; :: thesis: contradiction
then {_{X}_} <> {} by Th2;
hence contradiction by A1, A5; :: thesis: verum
end;
assume X = {} ; :: thesis: (.: R) .: {_{X}_} = {}
then {_{X}_} = {} by Th2;
hence (.: R) .: {_{X}_} = {} ; :: thesis: verum