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

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

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

end;

assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) ; :: thesis: V is prime
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def 6 :: thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
assume A4: X "/\" Y <= V ; :: thesis: ( X <= V or Y <= V )
X /\ Y = X "/\" Y by Th18;
then X /\ Y c= V by A4, YELLOW_1:3;
then ( X c= V or Y c= V ) by A3;
hence ( X <= V or Y <= V ) by YELLOW_1:3; :: thesis: verum