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 ; :: 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 ;
hence a in L | O by ; :: thesis: verum