let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: for a being Element of L st Top L <= a holds
a = Top L
let a be Element of L; :: thesis: ( Top L <= a implies a = Top L )
A1: a <= Top L by YELLOW_0:45;
assume Top L <= a ; :: thesis: a = Top L
hence a = Top L by A1, YELLOW_0:def 3; :: thesis: verum