let x, y be object ; :: according to ORDERS_2:def 4,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) and
A2: y in the carrier of (Omega T) and
A3: [x,y] in the InternalRel of (Omega T) and
A4: [y,x] in the InternalRel of (Omega T) ; :: thesis: x = y
reconsider a = x, b = y as Element of (Omega T) by A1, A2;
b <= a by A4;
then A5: ex Y1 being Subset of T st
( Y1 = {a} & b in Cl Y1 ) 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 t1 = x, t2 = y as Element of T by A1, A2;
a <= b by A3;
then ex Y2 being Subset of T st
( Y2 = {b} & a in Cl Y2 ) by Def2;
then 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 A5, YELLOW14:21;
hence x = y by T_0TOPSP:def 7; :: thesis: verum