let X be set ; :: thesis: for L being List of X
for O being Operation of X
for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let L be List of X; :: thesis: for O being Operation of X
for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let O be Operation of X; :: thesis: for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let a be Element of X; :: thesis: ( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )

hereby :: thesis: ( ex b being Element of X st
( a in b . O & b in L ) implies a in L | O )

assume a in L | O ; :: thesis: ex b being Element of X st
( a in b . O & b in L )
then consider b being object such that
A1: ( [b,a] in O & b in L ) by RELAT_1:def 13;
reconsider b = b as Element of X by A1;
take b = b; :: thesis: ( a in b . O & b in L )
thus a in b . O by A1, RELAT_1:169; :: thesis: b in L
thus b in L by A1; :: thesis: verum

end;

given b being Element of X such that A2: ( a in b . O & b in L ) ; :: thesis: a in L | O
[b,a] in O by A2, RELAT_1:169;
hence a in L | O by A2, RELAT_1:def 13; :: thesis: verum