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: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
A3: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
A4: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A5: X is upper by A1, A3, WAYBEL11:31;

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

assume A6: 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 that
A7: v in X and
A8: 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 A3, A4, A2, PRE_TOPC:def 2;
w <= w ;
then w in downarrow w by WAYBEL_0:17;
then not V c= (downarrow w) ` by A1, A8, XBOOLE_0:def 5;
then A9: not V <= mdw by YELLOW_1:3;
v <= v ;
then v in downarrow v by WAYBEL_0:17;
then not V c= (downarrow v) ` by A1, A7, XBOOLE_0:def 5;
then not V <= mdv by YELLOW_1:3;
then not V <= mdv "\/" mdw by A3, A6, A9, Th14;
then A10: not V c= mdv "\/" mdw by YELLOW_1:3;
take z = v "/\" w; :: thesis: ( z in X & z <= v & z <= w )
A11: mdv \/ mdw = ((downarrow v) /\ (downarrow w)) ` by XBOOLE_1:54
.= (downarrow (v "/\" w)) ` by Th3 ;
mdv \/ mdw c= mdv "\/" mdw by A3, YELLOW_1:6;
then not V c= mdv \/ mdw by A10;
then X meets ((downarrow (v "/\" w)) `) ` by A1, A11, SUBSET_1:24;
then X /\ (((downarrow (v "/\" w)) `) `) <> {} ;
then consider zz being object such that
A12: zz in X /\ (downarrow (v "/\" w)) by XBOOLE_0:def 1;
A13: zz in downarrow (v "/\" w) by A12, XBOOLE_0:def 4;
A14: zz in X by A12, XBOOLE_0:def 4;
reconsider zz = zz as Element of L by A12;
zz <= v "/\" w by A13, WAYBEL_0:17;
hence z in X by A5, A14; :: thesis: ( z <= v & z <= w )
thus ( z <= v & z <= w ) by YELLOW_0:23; :: thesis: verum

end;

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

end;

assume A15: ( 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
A16: V <= Xx "\/" Y and
A17: not V <= Xx and
A18: not V <= Y by A3, Th14;
( Xx in sigma L & Y in sigma L ) by A4;
then reconsider Xx9 = Xx, Y9 = Y as Subset of L ;
A19: Y9 is open by A3, A4, A2, PRE_TOPC:def 2;
then A20: Y9 is upper by WAYBEL11:def 4;
A21: Xx9 is open by A3, A4, A2, PRE_TOPC:def 2;
then Xx9 \/ Y9 is open by A19;
then Xx \/ Y in sigma L by A3, A2, PRE_TOPC:def 2;
then Xx \/ Y = Xx "\/" Y by YELLOW_1:8;
then A22: V c= Xx \/ Y by A16, YELLOW_1:3;
not V c= Y by A18, YELLOW_1:3;
then consider w being object such that
A23: w in V and
A24: not w in Y ;
not V c= Xx by A17, YELLOW_1:3;
then consider v being object such that
A25: v in V and
A26: not v in Xx ;
reconsider v = v, w = w as Element of L by A1, A25, A23;
A27: Xx9 is upper by A21, WAYBEL11:def 4;

A28: now :: thesis: not v "/\" w in Xx9 \/ Y9

assume A29: v "/\" w in Xx9 \/ Y9 ; :: thesis: contradiction

per cases ( v "/\" w in Xx9 or v "/\" w in Y9 ) by A29, XBOOLE_0:def 3;

suppose A30: v "/\" w in Xx9 ; :: thesis: contradiction

v "/\" w <= v by YELLOW_0:23;
hence contradiction by A26, A27, A30; :: thesis: verum

end;

suppose A31: v "/\" w in Y9 ; :: thesis: contradiction

v "/\" w <= w by YELLOW_0:23;
hence contradiction by A24, A20, A31; :: thesis: verum

end;

end;

end;

v "/\" w in X by A1, A15, A25, A23, WAYBEL_0:41;
hence contradiction by A1, A22, A28; :: thesis: verum