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

proof

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

end;

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

proof

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

end;