let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
let R be RMembership_Func of X,X; :: thesis: for Q being Subset of
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
let Q be Subset of ; :: thesis: for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
let x, z be Element of X; :: thesis: { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
set FL = FuzzyLattice [:X,X:];
set A = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } ;
set B = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z];
thus { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } c= pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] :: according to XBOOLE_0:def 10 :: thesis: pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] c= { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } or a in pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] )
assume a in { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } ; :: thesis: a in pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
then consider r being Element of such that
A1: a = (R (#) (@ r)) . [x,z] and
A2: r in Q ;
R (#) (@ r) in { (R (#) (@ r')) where r' is Element of : r' in Q } by A2;
hence a in pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] by A1, CARD_3:def 6; :: thesis: verum

end;

thus pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] c= { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] or b in { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } )
assume b in pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z] ; :: thesis: b in { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
then consider f being Function such that
A3: f in { (R (#) (@ r')) where r' is Element of : r' in Q } and
A4: b = f . [x,z] by CARD_3:def 6;
ex r being Element of st
( f = R (#) (@ r) & r in Q ) by A3;
hence b in { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } by A4; :: thesis: verum

end;