let L be complete Scott TopLattice; :: thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let X be Subset of L; :: thesis: for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let V be Element of (InclPoset (sigma L)); :: thesis: ( V = X implies ( V is co-prime iff ( X is filtered & X is upper ) ) )
assume A1: V = X ; :: thesis: ( V is co-prime iff ( X is filtered & X is upper ) )
A2: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
A3: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A4: X is upper by A1, A2, WAYBEL11:31;
A5: TopStruct(# the carrier of L,the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;

hereby :: thesis: ( X is filtered & X is upper implies V is co-prime )

assume A7: V is co-prime ; :: thesis: ( X is filtered & X is upper )
thus X is filtered :: thesis: X is upper

proof

let v, w be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not v in X or not w in X or ex b₁ being Element of the carrier of L st
( b₁ in X & b₁ <= v & b₁ <= w ) )
assume A8: ( v in X & w in X ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in X & b₁ <= v & b₁ <= w )
( (downarrow w) ` is open & (downarrow v) ` is open ) by WAYBEL11:12;
then reconsider mdw = (downarrow w) ` , mdv = (downarrow v) ` as Element of (InclPoset (sigma L)) by A2, A3, A5, PRE_TOPC:def 5;
( v <= v & w <= w ) ;
then ( v in downarrow v & w in downarrow w ) by WAYBEL_0:17;
then ( not V c= (downarrow v) ` & not V c= (downarrow w) ` ) by A1, A8, XBOOLE_0:def 5;
then ( not V <= mdv & not V <= mdw ) by YELLOW_1:3;
then not V <= mdv "\/" mdw by A2, A7, Th14;
then A9: not V c= mdv "\/" mdw by YELLOW_1:3;
mdv \/ mdw c= mdv "\/" mdw by A2, YELLOW_1:6;
then A10: not V c= mdv \/ mdw by A9, XBOOLE_1:1;
mdv \/ mdw = ((downarrow v) /\ (downarrow w)) ` by XBOOLE_1:54
.= (downarrow (v "/\" w)) ` by Th3 ;
then X meets ((downarrow (v "/\" w)) ` ) ` by A1, A10, SUBSET_1:44;
then X /\ (((downarrow (v "/\" w)) ` ) ` ) <> {} by XBOOLE_0:def 7;
then consider zz being set such that
A11: zz in X /\ (downarrow (v "/\" w)) by XBOOLE_0:def 1;
A12: ( zz in X & zz in downarrow (v "/\" w) ) by A11, XBOOLE_0:def 4;
reconsider zz = zz as Element of L by A11;
A13: zz <= v "/\" w by A12, WAYBEL_0:17;
take z = v "/\" w; :: thesis: ( z in X & z <= v & z <= w )
thus z in X by A4, A12, A13, WAYBEL_0:def 20; :: thesis: ( z <= v & z <= w )
thus ( z <= v & z <= w ) by YELLOW_0:23; :: thesis: verum

end;

thus X is upper by A1, A2, A3, WAYBEL11:31; :: thesis: verum

end;

assume A14: ( X is filtered & X is upper ) ; :: thesis: V is co-prime
assume not V is co-prime ; :: thesis: contradiction
then consider Xx, Y being Element of (InclPoset (sigma L)) such that
A15: ( V <= Xx "\/" Y & not V <= Xx & not V <= Y ) by A2, Th14;
( Xx in sigma L & Y in sigma L ) by A3;
then reconsider Xx' = Xx, Y' = Y as Subset of L ;
A16: ( Xx' is open & Y' is open ) by A2, A3, A5, PRE_TOPC:def 5;
then Xx' \/ Y' is open by TOPS_1:37;
then Xx \/ Y in sigma L by A2, A5, PRE_TOPC:def 5;
then Xx \/ Y = Xx "\/" Y by YELLOW_1:8;
then A17: V c= Xx \/ Y by A15, YELLOW_1:3;
A18: ( not V c= Xx & not V c= Y ) by A15, YELLOW_1:3;
then consider v being set such that
A19: ( v in V & not v in Xx ) by TARSKI:def 3;
consider w being set such that
A20: ( w in V & not w in Y ) by A18, TARSKI:def 3;
A21: ( Xx' is upper & Y' is upper ) by A16, WAYBEL11:def 4;
reconsider v = v, w = w as Element of L by A1, A19, A20;

A22: now

assume A23: v "/\" w in Xx' \/ Y' ; :: thesis: contradiction

per cases ( v "/\" w in Xx' or v "/\" w in Y' ) by A23, XBOOLE_0:def 3;

suppose A24: v "/\" w in Xx' ; :: thesis: contradiction

v "/\" w <= v by YELLOW_0:23;
hence contradiction by A19, A21, A24, WAYBEL_0:def 20; :: thesis: verum

end;

suppose A25: v "/\" w in Y' ; :: thesis: contradiction

v "/\" w <= w by YELLOW_0:23;
hence contradiction by A20, A21, A25, WAYBEL_0:def 20; :: thesis: verum

end;

end;

end;

v "/\" w in X by A1, A14, A19, A20, WAYBEL_0:41;
hence contradiction by A1, A17, A22; :: thesis: verum