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

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

let u be Element of (); :: thesis: ( (@ u) ^ {a} = {} implies (Atom A) . a [= () . u )
assume A1: (@ u) ^ {a} = {} ; :: thesis: (Atom A) . 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 () . 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 () . u & e c= c ) )

assume c in (Atom A) . a ; :: thesis: ex e being Element of DISJOINT_PAIRS A st
( e in () . 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 ;
consider d being Element of DISJOINT_PAIRS A such that
A4: d c= b and
A5: d in mi (- (@ u)) by ;
take e = d; :: thesis: ( e in () . u & e c= c )
thus e in () . u by ; :: thesis: e c= c
thus e c= c by ; :: thesis: verum
end;
hence (Atom A) . a [= () . u by Lm3; :: thesis: verum