let C be FormalContext; :: thesis: ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
set G = rng (gamma C);
thus rng (gamma C) is supremum-dense :: thesis: rng (delta C) is infimum-dense
proof
let a be Element of (ConceptLattice C); :: according to LATTICE6:def 13 :: thesis: ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(ConceptLattice C))
A1: { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } c= rng (gamma C)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } or x in rng (gamma C) )
assume x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ; :: thesis: x in rng (gamma C)
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A2: x = ConceptStr(# O,A #) and
A3: ex o being Object of C st
( o in the Extent of (a @) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ;
consider o being Object of C such that
o in the Extent of (a @) and
O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) and
A4: A = (ObjectDerivation C) . {o} by A3;
consider y being Element of (ConceptLattice C) such that
A5: (gamma C) . o = y ;
( dom (gamma C) = the carrier of C & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( y = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A9 = (ObjectDerivation C) . {o} ) ) by A5, Def4, FUNCT_2:def 1;
hence x in rng (gamma C) by A2, A3, A4, A5, FUNCT_1:def 3; :: thesis: verum
end;
( "\/" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(ConceptLattice C)) = a @ & a = a @ ) by Th9, CONLAT_1:def 21;
hence ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(ConceptLattice C)) by A1; :: thesis: verum
end;
let b be Element of (ConceptLattice C); :: according to LATTICE6:def 14 :: thesis: ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(ConceptLattice C))
set G = rng (delta C);
A6: { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } c= rng (delta C)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } or x in rng (delta C) )
assume x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ; :: thesis: x in rng (delta C)
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A7: x = ConceptStr(# O,A #) and
A8: ex a being Attribute of C st
( a in the Intent of (b @) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ;
consider a being Attribute of C such that
a in the Intent of (b @) and
A9: O = (AttributeDerivation C) . {a} and
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by A8;
consider y being Element of (ConceptLattice C) such that
A10: (delta C) . a = y ;
( dom (delta C) = the carrier' of C & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( y = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . {a} & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) by A10, Def5, FUNCT_2:def 1;
hence x in rng (delta C) by A7, A8, A9, A10, FUNCT_1:def 3; :: thesis: verum
end;
( "/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = b @ & b = b @ ) by Th10, CONLAT_1:def 21;
hence ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(ConceptLattice C)) by A6; :: thesis: verum