let x, y, z be object ; ORDERS_2:def 3,RELAT_2:def 8 ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not z in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,z] in the InternalRel of (Omega T) or [x,z] in the InternalRel of (Omega T) )
assume that
A1:
x in the carrier of (Omega T)
and
A2:
y in the carrier of (Omega T)
and
A3:
z in the carrier of (Omega T)
and
A4:
[x,y] in the InternalRel of (Omega T)
and
A5:
[y,z] in the InternalRel of (Omega T)
; [x,z] in the InternalRel of (Omega T)
reconsider a = x, b = y, c = z as Element of (Omega T) by A1, A2, A3;
a <= b
by A4;
then consider Y2 being Subset of T such that
A6:
Y2 = {b}
and
A7:
a in Cl Y2
by Def2;
TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #)
by Def2;
then reconsider t3 = z as Element of T by A3;
b <= c
by A5;
then consider Y3 being Subset of T such that
A8:
Y3 = {c}
and
A9:
b in Cl Y3
by Def2;
Y3 = {t3}
by A8;
then
Cl Y2 c= Cl Y3
by A6, A9, Lm2;
then
a <= c
by A7, A8, Def2;
hence
[x,z] in the InternalRel of (Omega T)
; verum