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
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 )
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;
hence (Atom A) . a [= (pseudo_compl A) . u by Lm3; :: thesis: verum