let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p is valid holds

X |- p

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st p is valid holds

X |- p

let p be Element of CQC-WFF Al; :: thesis: ( p is valid implies X |- p )

assume p is valid ; :: thesis: X |- p

then A1: p in TAUT Al ;

TAUT Al c= Cn X by Th11, Th34;

hence X |- p by A1; :: thesis: verum

for p being Element of CQC-WFF Al st p is valid holds

X |- p

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st p is valid holds

X |- p

let p be Element of CQC-WFF Al; :: thesis: ( p is valid implies X |- p )

assume p is valid ; :: thesis: X |- p

then A1: p in TAUT Al ;

TAUT Al c= Cn X by Th11, Th34;

hence X |- p by A1; :: thesis: verum