let x, y be set ; :: according to ORDERS_2:def 6,RELAT_2:def 4 :: thesis: ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,x] in the InternalRel of (Omega T) or x = y )
assume that
A1: ( x in the carrier of (Omega T) & y in the carrier of (Omega T) ) and
A2: [x,y] in the InternalRel of (Omega T) and
A3: [y,x] in the InternalRel of (Omega T) ; :: thesis: x = y
reconsider a = x, b = y as Element of (Omega T) by A1;
TopStruct(# the carrier of (Omega T),the topology of (Omega T) #) = TopStruct(# the carrier of T,the topology of T #) by Def2;
then reconsider t1 = x, t2 = y as Element of T by A1;
a <= b by A2, ORDERS_2:def 9;
then consider Y2 being Subset of T such that
A4: Y2 = {b} and
A5: a in Cl Y2 by Def2;
b <= a by A3, ORDERS_2:def 9;
then consider Y1 being Subset of T such that
A6: Y1 = {a} and
A7: b in Cl Y1 by Def2;
for V being Subset of T holds
( not V is open or ( ( t1 in V implies t2 in V ) & ( t2 in V implies t1 in V ) ) ) by A4, A5, A6, A7, YELLOW14:22;
hence x = y by T_0TOPSP:def 7; :: thesis: verum