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 <> {} ) )
hereby :: thesis: ( x in L & x . O <> {} implies x in L WHERE O )
assume 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;
assume A2: ( x in L & x . O <> {} ) ; :: thesis: x in L WHERE 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