let X be set ; :: thesis: for L being List of X

for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O

let L be List of X; :: thesis: for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O

let O, O1 be Operation of X; :: thesis: L WHEREgt (O,O1) c= L WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHEREgt (O,O1) or z in L WHERE O )

assume z in L WHEREgt (O,O1) ; :: thesis: z in L WHERE O

then consider x being Element of X such that

A1: ( z = x & card (x . O1) in card (x . O) & x in L ) ;

x . O <> {} by A1;

hence z in L WHERE O by A1, Th3; :: thesis: verum

for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O

let L be List of X; :: thesis: for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O

let O, O1 be Operation of X; :: thesis: L WHEREgt (O,O1) c= L WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHEREgt (O,O1) or z in L WHERE O )

assume z in L WHEREgt (O,O1) ; :: thesis: z in L WHERE O

then consider x being Element of X such that

A1: ( z = x & card (x . O1) in card (x . O) & x in L ) ;

x . O <> {} by A1;

hence z in L WHERE O by A1, Th3; :: thesis: verum