let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A

for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds

(Atom A) . a [= (pseudo_compl A) . u

let a be Element of DISJOINT_PAIRS A; :: thesis: for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds

(Atom A) . a [= (pseudo_compl A) . u

let u be Element of (NormForm A); :: thesis: ( (@ u) ^ {a} = {} implies (Atom A) . a [= (pseudo_compl A) . u )

assume A1: (@ u) ^ {a} = {} ; :: thesis: (Atom A) . a [= (pseudo_compl A) . u

for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds

(Atom A) . a [= (pseudo_compl A) . u

let a be Element of DISJOINT_PAIRS A; :: thesis: for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds

(Atom A) . a [= (pseudo_compl A) . u

let u be Element of (NormForm A); :: thesis: ( (@ u) ^ {a} = {} implies (Atom A) . a [= (pseudo_compl A) . u )

assume A1: (@ u) ^ {a} = {} ; :: thesis: (Atom A) . a [= (pseudo_compl A) . u

now :: thesis: for c being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds

ex e being Element of DISJOINT_PAIRS A st

( e in (pseudo_compl A) . u & e c= c )

hence
(Atom A) . a [= (pseudo_compl A) . u
by Lm3; :: thesis: verumex e being Element of DISJOINT_PAIRS A st

( e in (pseudo_compl A) . u & e c= c )

let c be Element of DISJOINT_PAIRS A; :: thesis: ( c in (Atom A) . a implies ex e being Element of DISJOINT_PAIRS A st

( e in (pseudo_compl A) . u & e c= c ) )

assume c in (Atom A) . a ; :: thesis: ex e being Element of DISJOINT_PAIRS A st

( e in (pseudo_compl A) . u & e c= c )

then c = a by Th6;

then consider b being Element of DISJOINT_PAIRS A such that

A2: b in - (@ u) and

A3: b c= c by A1, Th19;

consider d being Element of DISJOINT_PAIRS A such that

A4: d c= b and

A5: d in mi (- (@ u)) by A2, NORMFORM:41;

take e = d; :: thesis: ( e in (pseudo_compl A) . u & e c= c )

thus e in (pseudo_compl A) . u by A5, Def8; :: thesis: e c= c

thus e c= c by A3, A4, NORMFORM:2; :: thesis: verum

end;( e in (pseudo_compl A) . u & e c= c ) )

assume c in (Atom A) . a ; :: thesis: ex e being Element of DISJOINT_PAIRS A st

( e in (pseudo_compl A) . u & e c= c )

then c = a by Th6;

then consider b being Element of DISJOINT_PAIRS A such that

A2: b in - (@ u) and

A3: b c= c by A1, Th19;

consider d being Element of DISJOINT_PAIRS A such that

A4: d c= b and

A5: d in mi (- (@ u)) by A2, NORMFORM:41;

take e = d; :: thesis: ( e in (pseudo_compl A) . u & e c= c )

thus e in (pseudo_compl A) . u by A5, Def8; :: thesis: e c= c

thus e c= c by A3, A4, NORMFORM:2; :: thesis: verum