let T be complete continuous Scott TopLattice; :: thesis: for p being Element of T holds Int (uparrow p) = wayabove p
let p be Element of T; :: thesis: Int (uparrow p) = wayabove p
thus Int (uparrow p) c= wayabove p :: according to XBOOLE_0:def 10 :: thesis: wayabove p c= Int (uparrow p)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Int (uparrow p) or y in wayabove p )
assume A1: y in Int (uparrow p) ; :: thesis: y in wayabove p
then reconsider q = y as Element of T ;
reconsider S = Int (uparrow p) as Subset of T ;
consider u being Element of T such that
A2: u << q and
A3: u in S by A1, Th43;
S c= uparrow p by TOPS_1:16;
then p <= u by A3, WAYBEL_0:18;
then p << q by A2, WAYBEL_3:2;
hence y in wayabove p ; :: thesis: verum
end;
wayabove p c= uparrow p by WAYBEL_3:11;
hence wayabove p c= Int (uparrow p) by Th36, TOPS_1:24; :: thesis: verum