let A be Subset of T; :: thesis: ( A in BB & inf F in A implies F opp+id is_eventually_in A )
assume that
A3: A in BB and
A4: inf F in A ; :: thesis: F opp+id is_eventually_in A
A is open by A3, TOPS_2:def 1;
then A5: A is lower by Th5;
F meets A by A3, A4, A1;
then consider i being object such that
A6: i in F and
A7: i in A by XBOOLE_0:3;
reconsider i = i as Element of (F opp+id) by A6, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (F opp+id) holds
( not i <= b₁ or (F opp+id) . b₁ in A )
let j be Element of (F opp+id); :: thesis: ( not i <= j or (F opp+id) . j in A )
A8: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider a = i, b = j as Element of (T opp) by YELLOW_0:58;
assume i <= j ; :: thesis: (F opp+id) . j in A
then a <= b by A8, YELLOW_0:59;
then A9: ~ b <= ~ a by YELLOW_7:1;
(F opp+id) . j = j by YELLOW_9:7;
hence (F opp+id) . j in A by A9, A7, A5; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (netmap ((F opp+id),T)) or x in F )
assume x in rng (netmap ((F opp+id),T)) ; :: thesis: x in F
then consider a being object such that
A11: a in dom (netmap ((F opp+id),T)) and
A12: x = (netmap ((F opp+id),T)) . a by FUNCT_1:def 3;
reconsider a = a as Element of (F opp+id) by A11;
x = (F opp+id) . a by A12
.= a by YELLOW_9:7 ;
hence x in F by A10; :: thesis: verum