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 that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: 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 object st a in waybelow y holds
a in waybelow x
let a be object ; :: 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
A3: a = z and
A4: 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, A4, WAYBEL_8:8;
hence a in waybelow y by A3; :: thesis: verum
end;
let a be object ; :: 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
A5: a = z and
A6: 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, A2, A6, WAYBEL_8:8;
hence a in waybelow x by A5; :: thesis: verum
end;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: wayabove y c= wayabove x
let a be object ; :: 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
A7: a = z and
A8: 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, A8, WAYBEL_8:8;
hence a in wayabove y by A7; :: thesis: verum
end;
let a be object ; :: 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
A9: a = z and
A10: 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, A2, A10, WAYBEL_8:8;
hence a in wayabove x by A9; :: thesis: verum