let A1, A2 be Relation of L; ( ( for x, y being Element of L holds
( [x,y] in A1 iff x << y ) ) & ( for x, y being Element of L holds
( [x,y] in A2 iff x << y ) ) implies A1 = A2 )
assume A2:
for x, y being Element of L holds
( [x,y] in A1 iff x << y )
; ( ex x, y being Element of L st
( ( [x,y] in A2 implies x << y ) implies ( x << y & not [x,y] in A2 ) ) or A1 = A2 )
assume A3:
for x, y being Element of L holds
( [x,y] in A2 iff x << y )
; A1 = A2
thus
A1 = A2
verumproof
let a,
b be
object ;
RELAT_1:def 2 ( ( not [a,b] in A1 or [a,b] in A2 ) & ( not [a,b] in A2 or [a,b] in A1 ) )
hereby ( not [a,b] in A2 or [a,b] in A1 )
end;
assume A5:
[a,b] in A2
;
[a,b] in A1
then reconsider a9 =
a,
b9 =
b as
Element of
L by ZFMISC_1:87;
a9 << b9
by A3, A5;
hence
[a,b] in A1
by A2;
verum
end;