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 ) )

[b,a] in O by A2, RELAT_1:169;

hence a in L | O by A2, RELAT_1:def 13; :: thesis: verum

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 )

given b being Element of X such that A2:
( a in b . O & b in L )
; :: thesis: a in L | O( 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;( 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

[b,a] in O by A2, RELAT_1:169;

hence a in L | O by A2, RELAT_1:def 13; :: thesis: verum