let L1 be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for L2 being non empty reflexive RelStr
for x being Element of L1
for y being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y holds
( waybelow x = waybelow y & wayabove x = wayabove y )
let L2 be non empty reflexive RelStr ; :: thesis: for x being Element of L1
for y being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y holds
( waybelow x = waybelow y & wayabove x = wayabove y )
let x be Element of L1; :: thesis: for y being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y holds
( waybelow x = waybelow y & wayabove x = wayabove y )
let y be Element of L2; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y implies ( waybelow x = waybelow y & wayabove x = wayabove y ) )
assume A1: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y ) ; :: thesis: ( waybelow x = waybelow y & wayabove x = wayabove y )

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: wayabove x = wayabove y

hereby :: thesis: for a being set st a in waybelow y holds
a in waybelow x

let a be set ; :: thesis: ( a in waybelow x implies a in waybelow y )
assume a in waybelow x ; :: thesis: a in waybelow y
then consider z being Element of L1 such that
A2: ( a = z & z << x ) ;
reconsider w = z as Element of L2 by A1;
L2 is antisymmetric by A1, WAYBEL_8:14;
then w << y by A1, A2, WAYBEL_8:8;
hence a in waybelow y by A2; :: thesis: verum

end;

let a be set ; :: thesis: ( a in waybelow y implies a in waybelow x )
assume a in waybelow y ; :: thesis: a in waybelow x
then consider z being Element of L2 such that
A3: ( a = z & z << y ) ;
reconsider w = z as Element of L1 by A1;
( L2 is up-complete & L2 is antisymmetric ) by A1, WAYBEL_8:14, WAYBEL_8:15;
then w << x by A1, A3, WAYBEL_8:8;
hence a in waybelow x by A3; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: wayabove y c= wayabove x

let a be set ; :: thesis: ( a in wayabove x implies a in wayabove y )
assume a in wayabove x ; :: thesis: a in wayabove y
then consider z being Element of L1 such that
A4: ( a = z & z >> x ) ;
reconsider w = z as Element of L2 by A1;
L2 is antisymmetric by A1, WAYBEL_8:14;
then w >> y by A1, A4, WAYBEL_8:8;
hence a in wayabove y by A4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in wayabove y or a in wayabove x )
assume a in wayabove y ; :: thesis: a in wayabove x
then consider z being Element of L2 such that
A5: ( a = z & z >> y ) ;
reconsider w = z as Element of L1 by A1;
( L2 is up-complete & L2 is antisymmetric ) by A1, WAYBEL_8:14, WAYBEL_8:15;
then w >> x by A1, A5, WAYBEL_8:8;
hence a in wayabove x by A5; :: thesis: verum