let T be non empty TopSpace; :: thesis: for V being Element of (InclPoset the topology of T) holds
( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
let V be Element of (InclPoset the topology of T); :: thesis: ( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )

hereby :: thesis: ( ( for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ) implies V is co-prime )

assume A1: V is co-prime ; :: thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y )
let X, Y be Element of (InclPoset the topology of T); :: thesis: ( not V c= X \/ Y or V c= X or V c= Y )
assume A2: V c= X \/ Y ; :: thesis: ( V c= X or V c= Y )
X \/ Y = X "\/" Y by Th18;
then V <= X "\/" Y by A2, YELLOW_1:3;
then ( V <= X or V <= Y ) by A1, Th14;
hence ( V c= X or V c= Y ) by YELLOW_1:3; :: thesis: verum

end;

assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ; :: thesis: V is co-prime

now :: thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not V <= X "\/" Y or V <= X or V <= Y )

let X, Y be Element of (InclPoset the topology of T); :: thesis: ( not V <= X "\/" Y or V <= X or V <= Y )
assume A4: V <= X "\/" Y ; :: thesis: ( V <= X or V <= Y )
X \/ Y = X "\/" Y by Th18;
then V c= X \/ Y by A4, YELLOW_1:3;
then ( V c= X or V c= Y ) by A3;
hence ( V <= X or V <= Y ) by YELLOW_1:3; :: thesis: verum

end;

hence V is co-prime by Th14; :: thesis: verum