let A1, A2 be Relation of L; :: thesis: ( ( for x, y being Element of L holds
( [x,y] in A1 iff x = Bottom L ) ) & ( for x, y being Element of L holds
( [x,y] in A2 iff x = Bottom L ) ) implies A1 = A2 )
assume A2: for x, y being Element of L holds
( [x,y] in A1 iff x = Bottom L ) ; :: thesis: ( ex x, y being Element of L st
( ( [x,y] in A2 implies x = Bottom L ) implies ( x = Bottom L & not [x,y] in A2 ) ) or A1 = A2 )
assume A3: for x, y being Element of L holds
( [x,y] in A2 iff x = Bottom L ) ; :: thesis: A1 = A2
thus A1 = A2 :: thesis: verum

proof

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in A1 or [a,b] in A2 ) & ( not [a,b] in A2 or [a,b] in A1 ) )

hereby :: thesis: ( not [a,b] in A2 or [a,b] in A1 )

assume A4: [a,b] in A1 ; :: thesis: [a,b] in A2
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
[a9,b9] in A1 by A4;
then a9 = Bottom L by A2;
then [a9,b9] in A2 by A3;
hence [a,b] in A2 ; :: thesis: verum

end;

assume A5: [a,b] in A2 ; :: thesis: [a,b] in A1
then reconsider a9 = a, b9 = b as Element of L by ZFMISC_1:87;
[a9,b9] in A2 by A5;
then a9 = Bottom L by A3;
then [a9,b9] in A1 by A2;
hence [a,b] in A1 ; :: thesis: verum

end;