{ x where x is Element of X : ( card (x . O) = n & x in L ) } c= X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of X : ( card (x . O) = n & x in L ) } or z in X )
assume z in { x where x is Element of X : ( card (x . O) = n & x in L ) } ; :: thesis: z in X
then ex x being Element of X st
( z = x & card (x . O) = n & x in L ) ;
hence z in X ; :: thesis: verum
end;
hence { x where x is Element of X : ( card (x . O) = n & x in L ) } is List of X ; :: thesis: verum