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 set ; :: 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] & r in Q ) ;
R (#) (@ r) in { (R (#) (@ r')) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q } by A1;
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 set ; :: 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
A2: ( f in { (R (#) (@ r')) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q } & b = f . [x,z] ) by CARD_3:def 6;
consider r being Element of (FuzzyLattice [:X,X:]) such that
A3: ( f = R (#) (@ r) & r in Q ) by A2;
thus b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A2, A3; :: thesis: verum

end;