let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
A1: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then ( x in the topology of T & y in the topology of T ) ;
then reconsider x9 = x, y9 = y as Subset of T ;
( x9 is open & y9 is open ) by A1, PRE_TOPC:def 2;
then x9 \/ y9 is open ;
then x9 \/ y9 in the topology of T by PRE_TOPC:def 2;
hence x "\/" y = x \/ y by YELLOW_1:8; :: thesis: x "/\" y = x /\ y
x9 /\ y9 in the topology of T by A1, PRE_TOPC:def 1;
hence x "/\" y = x /\ y by YELLOW_1:9; :: thesis: verum