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

for x being Element of X

for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let L be List of X; :: thesis: for x being Element of X

for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let x be Element of X; :: thesis: for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let O be Operation of X; :: thesis: ( x in L WHERE O iff ( x in L & x . O <> {} ) )

set y = the Element of x . O;

the Element of x . O in x . O by A2;

then reconsider y = the Element of x . O as Element of X ;

x,y in O by A2, Th2;

hence x in L WHERE O by A2; :: thesis: verum

for x being Element of X

for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let L be List of X; :: thesis: for x being Element of X

for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let x be Element of X; :: thesis: for O being Operation of X holds

( x in L WHERE O iff ( x in L & x . O <> {} ) )

let O be Operation of X; :: thesis: ( x in L WHERE O iff ( x in L & x . O <> {} ) )

hereby :: thesis: ( x in L & x . O <> {} implies x in L WHERE O )

assume A2:
( x in L & x . O <> {} )
; :: thesis: x in L WHERE Oassume
x in L WHERE O
; :: thesis: ( x in L & x . O <> {} )

then consider y being Element of X such that

A1: ( x = y & ex a being Element of X st

( y,a in O & y in L ) ) ;

thus ( x in L & x . O <> {} ) by A1, Th2; :: thesis: verum

end;then consider y being Element of X such that

A1: ( x = y & ex a being Element of X st

( y,a in O & y in L ) ) ;

thus ( x in L & x . O <> {} ) by A1, Th2; :: thesis: verum

set y = the Element of x . O;

the Element of x . O in x . O by A2;

then reconsider y = the Element of x . O as Element of X ;

x,y in O by A2, Th2;

hence x in L WHERE O by A2; :: thesis: verum