let x be object ; :: according to ORDERS_2:def 2,RELAT_2:def 1 :: thesis: ( not x in the carrier of (Omega T) or [x,x] in the InternalRel of (Omega T) )
assume A1: x in the carrier of (Omega T) ; :: thesis: [x,x] in the InternalRel of (Omega T)
then reconsider T9 = T as non empty TopStruct ;
reconsider a = x as Element of (Omega T) by A1;
reconsider t9 = x as Element of T9 by A1, Lm1;
consider Y being Subset of T such that
A2: Y = {t9} ;
A3: Y c= Cl Y by PRE_TOPC:18;
a in Y by A2, TARSKI:def 1;
then a <= a by A2, A3, Def2;
hence [x,x] in the InternalRel of (Omega T) ; :: thesis: verum