let x, y, z be set ; :: according to ORDERS_2:def 5,RELAT_2:def 8 :: thesis: ( 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) & y in the carrier of (Omega T) & z in the carrier of (Omega T) ) and
A2: [x,y] in the InternalRel of (Omega T) and
A3: [y,z] in the InternalRel of (Omega T) ; :: thesis: [x,z] in the InternalRel of (Omega T)
A4: TopStruct(# the carrier of (Omega T),the topology of (Omega T) #) = TopStruct(# the carrier of T,the topology of T #) by Def2;
reconsider a = x, b = y, c = z as Element of (Omega T) by A1;
reconsider t2 = y, t3 = z as Element of T by A1, A4;
a <= b by A2, ORDERS_2:def 9;
then consider Y2 being Subset of T such that
A5: Y2 = {b} and
A6: a in Cl Y2 by Def2;
b <= c by A3, ORDERS_2:def 9;
then consider Y3 being Subset of T such that
A7: Y3 = {c} and
A8: b in Cl Y3 by Def2;
( Y2 = {t2} & Y3 = {t3} ) by A5, A7;
then Cl Y2 c= Cl Y3 by A8, Lm2;
then a <= c by A6, A7, Def2;
hence [x,z] in the InternalRel of (Omega T) by ORDERS_2:def 9; :: thesis: verum